let F be non almost_trivial Field; :: thesis: ex K being non polynomial_disjoint Field st K,F are_isomorphic
set x = the non trivial Element of F;
reconsider o = <%(0. F),(1. F)%> as object ;

per cases ( not o in [#] F or ex a being Element of F st a = <%(0. F),(1. F)%> ) ;

suppose A1: not o in [#] F ; :: thesis: ex K being non polynomial_disjoint Field st K,F are_isomorphic

then reconsider S = ExField ( the non trivial Element of F,o) as Field by Th7, Th8, Th9, Th10, Th11, Th12;
([#] S) /\ ([#] (Polynom-Ring S)) <> {} by Th13;
then reconsider S = S as non polynomial_disjoint Field by Def3;
take S ; :: thesis: S,F are_isomorphic
( isoR ( the non trivial Element of F,o) is additive & isoR ( the non trivial Element of F,o) is multiplicative & isoR ( the non trivial Element of F,o) is unity-preserving ) by A1, Th15;
hence S,F are_isomorphic by MOD_4:def 12, QUOFIELD:def 23; :: thesis: verum

end;

suppose ex a being Element of F st a = <%(0. F),(1. F)%> ; :: thesis: ex K being non polynomial_disjoint Field st K,F are_isomorphic

then consider a being Element of F such that
A2: a = <%(0. F),(1. F)%> ;
a in [#] (Polynom-Ring F) by A2, POLYNOM3:def 10;
then a in ([#] F) /\ ([#] (Polynom-Ring F)) by XBOOLE_0:def 4;
then reconsider S = F as non polynomial_disjoint Field by Def3;
take S ; :: thesis: S,F are_isomorphic
thus S,F are_isomorphic ; :: thesis: verum

end;

end;