theorem :: FIELD_16:52

for F being finite Field holds F is PrimeField b₁ -simple FieldExtension of PrimeField F by FA1;