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 ;

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)%> )
;

end;

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;([#] 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

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;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