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 ;
([#] S) /\ ([#] ()) <> {} by Th13;
then reconsider S = S as non polynomial_disjoint Field by Def3;
take S ; :: thesis:
( 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 ;
hence S,F are_isomorphic by ; :: 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 [#] () by ;
then a in ([#] F) /\ ([#] ()) by XBOOLE_0:def 4;
then reconsider S = F as non polynomial_disjoint Field by Def3;
take S ; :: thesis:
thus S,F are_isomorphic ; :: thesis: verum
end;
end;