let K be Field; :: thesis: for F being K -monomorphic Field st K,F are_disjoint holds
ex E being Field st
( E,F are_isomorphic & K is Subfield of E )
let F be K -monomorphic Field; :: thesis: ( K,F are_disjoint implies ex E being Field st
( E,F are_isomorphic & K is Subfield of E ) )
assume AS: K,F are_disjoint ; :: thesis: ex E being Field st
( E,F are_isomorphic & K is Subfield of E )
set f = the Monomorphism of K,F;
reconsider E = embField the Monomorphism of K,F as Field by AS, Th6, Th8, Th9, Th7, Th10;
take E ; :: thesis: ( E,F are_isomorphic & K is Subfield of E )
thus ( E,F are_isomorphic & K is Subfield of E ) by AS, Th14, Th15; :: thesis: verum