let K be Field; :: thesis: for F being K -monomorphic Field
for f being Monomorphism of K,F
for E being Field st E = embField f holds
K is Subfield of E
let F be K -monomorphic Field; :: thesis: for f being Monomorphism of K,F
for E being Field st E = embField f holds
K is Subfield of E
let f be Monomorphism of K,F; :: thesis: for E being Field st E = embField f holds
K is Subfield of E
let E be Field; :: thesis: ( E = embField f implies K is Subfield of E )
A2: [#] (embField f) = carr f by defemb;
assume A1: E = embField f ; :: thesis: K is Subfield of E
then [#] E = carr f by defemb;
then A3: [#] K c= [#] E by XBOOLE_0:def 3;
A4: dom the addF of E = [:([#] E),([#] E):] by FUNCT_2:def 1;
set g1 = the addF of K;
set g2 = the addF of E | [:([#] K),([#] K):];
A5: dom ( the addF of E | [:([#] K),([#] K):]) = (dom the addF of E) /\ [:([#] K),([#] K):] by RELAT_1:61
.= [:([#] K),([#] K):] by A3, ZFMISC_1:96, XBOOLE_1:28, A4
.= dom the addF of K by FUNCT_2:def 1 ;

now :: thesis: for x being set st x in dom the addF of K holds
the addF of K . x = ( the addF of E | [:([#] K),([#] K):]) . x

let x be set ; :: thesis: ( x in dom the addF of K implies the addF of K . x = ( the addF of E | [:([#] K),([#] K):]) . x )
assume x in dom the addF of K ; :: thesis: the addF of K . x = ( the addF of E | [:([#] K),([#] K):]) . x
then consider x1, x2 being object such that
A6: ( x1 in [#] K & x2 in [#] K & x = [x1,x2] ) by ZFMISC_1:def 2;
reconsider a = x1, b = x2 as Element of K by A6;
A7: [a,b] in [:([#] K),([#] K):] by ZFMISC_1:def 2;
reconsider a1 = x1, b1 = x2 as Element of (embField f) by A6, A2, XBOOLE_0:def 3;
( the addF of E || ([#] K)) . (a,b) = a1 + b1 by A1, A7, FUNCT_1:49
.= a + b by Lm7 ;
hence the addF of K . x = ( the addF of E | [:([#] K),([#] K):]) . x by A6; :: thesis: verum

end;

then A8: the addF of K = the addF of E || ([#] K) by A5;
set g1 = the multF of K;
set g2 = the multF of E | [:([#] K),([#] K):];
A9: dom the multF of E = [:([#] E),([#] E):] by FUNCT_2:def 1;
A10: dom ( the multF of E | [:([#] K),([#] K):]) = (dom the multF of E) /\ [:([#] K),([#] K):] by RELAT_1:61
.= [:([#] K),([#] K):] by A3, ZFMISC_1:96, XBOOLE_1:28, A9
.= dom the multF of K by FUNCT_2:def 1 ;

now :: thesis: for x being set st x in dom the multF of K holds
the multF of K . x = ( the multF of E | [:([#] K),([#] K):]) . x

let x be set ; :: thesis: ( x in dom the multF of K implies the multF of K . x = ( the multF of E | [:([#] K),([#] K):]) . x )
assume x in dom the multF of K ; :: thesis: the multF of K . x = ( the multF of E | [:([#] K),([#] K):]) . x
then consider x1, x2 being object such that
A11: ( x1 in [#] K & x2 in [#] K & x = [x1,x2] ) by ZFMISC_1:def 2;
reconsider a = x1, b = x2 as Element of K by A11;
A12: [a,b] in [:([#] K),([#] K):] by ZFMISC_1:def 2;
reconsider a1 = x1, b1 = x2 as Element of (embField f) by A11, A2, XBOOLE_0:def 3;
( the multF of E || ([#] K)) . (a,b) = a1 * b1 by A1, A12, FUNCT_1:49
.= a * b by Lm11 ;
hence the multF of K . x = ( the multF of E | [:([#] K),([#] K):]) . x by A11; :: thesis: verum

end;

then A13: the multF of K = the multF of E || ([#] K) by A10;
( 1. E = 1. K & 0. E = 0. K ) by defemb, A1;
hence K is Subfield of E by A3, A8, A13, EC_PF_1:def 1; :: thesis: verum