theorem :: FIELD_3:20

for n being non zero Nat
for F being non almost_trivial Field ex K being non polynomial_disjoint Field ex p being Polynomial of K st
( K,F are_isomorphic & deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )