let E, F be Field; :: thesis: ( E includes F iff ex K being strict Subfield of E st K,F are_isomorphic )

hereby :: thesis: ( ex K being strict Subfield of E st K,F are_isomorphic implies E includes F )

assume A1: E includes F ; :: thesis: ex K being strict Subfield of E st K,F are_isomorphic
reconsider EE = E as Ring ;
consider K being strict Subring of EE such that
A2: K,F are_isomorphic by A1;
ex f being Function of F,K st f is RingIsomorphism by A2, QUOFIELD:def 23;
then reconsider KK = K as F -isomorphic Ring by Def4;
( the carrier of KK c= the carrier of E & the addF of KK = the addF of E || the carrier of KK & the multF of KK = the multF of E || the carrier of KK & 1. E = 1. KK & 0. E = 0. KK ) by C0SP1:def 3;
then KK is strict Subfield of E by EC_PF_1:def 1;
hence ex K being strict Subfield of E st K,F are_isomorphic by A2; :: thesis: verum

end;

given K being strict Subfield of E such that A3: K,F are_isomorphic ; :: thesis: E includes F
( the carrier of K c= the carrier of E & the addF of K = the addF of E || the carrier of K & the multF of K = the multF of E || the carrier of K & 1. E = 1. K & 0. E = 0. K ) by EC_PF_1:def 1;
then K is strict Subring of E by C0SP1:def 3;
hence E includes F by A3; :: thesis: verum