theorem CF: :: FIELD_15:92

for F being Field holds
( F is finite iff ex n being non zero Nat st card F = (Char F) |^ n )