theorem FA1: :: FIELD_16:51

for F being finite Field holds F is PrimeField b₁ -finite FieldExtension of PrimeField F