let K, F be Field; :: thesis: ( K,F are_disjoint implies ( F is K -monomorphic iff ex E being Field st
( E,F are_isomorphic & K is Subfield of E ) ) )
assume AS: K,F are_disjoint ; :: thesis: ( F is K -monomorphic iff ex E being Field st
( E,F are_isomorphic & K is Subfield of E ) )

now :: thesis: ( ex E being Field st
( E,F are_isomorphic & K is Subfield of E ) implies F is K -monomorphic )

assume ex E being Field st
( E,F are_isomorphic & K is Subfield of E ) ; :: thesis: F is K -monomorphic
then consider E being Field such that
A: ( E,F are_isomorphic & K is Subfield of E ) ;
K is Subring of E by A, RING_3:43;
then consider m being Function of K,E such that
B: ( m is RingHomomorphism & m is monomorphism ) by RING_3:def 3, RING_3:71;
consider i being Function of E,F such that
C: i is RingIsomorphism by A, QUOFIELD:def 23;
set f = i * m;
i * m is linear by B, C, RINGCAT1:1;
hence F is K -monomorphic by B, C, RING_3:def 3; :: thesis: verum

end;

hence ( F is K -monomorphic iff ex E being Field st
( E,F are_isomorphic & K is Subfield of E ) ) by AS, Th16; :: thesis: verum