let F be Field; :: thesis: for E being FieldExtension of F
for L being F -homomorphic b₁ -homomorphic Field
for f being Homomorphism of F,L
for g being Homomorphism of E,L st g is f -extending holds
Image f is Subfield of Image g
let E be FieldExtension of F; :: thesis: for L being F -homomorphic E -homomorphic Field
for f being Homomorphism of F,L
for g being Homomorphism of E,L st g is f -extending holds
Image f is Subfield of Image g
let L be F -homomorphic E -homomorphic Field; :: thesis: for f being Homomorphism of F,L
for g being Homomorphism of E,L st g is f -extending holds
Image f is Subfield of Image g
let f be Homomorphism of F,L; :: thesis: for g being Homomorphism of E,L st g is f -extending holds
Image f is Subfield of Image g
let g be Homomorphism of E,L; :: thesis: ( g is f -extending implies Image f is Subfield of Image g )
assume AS: g is f -extending ; :: thesis: Image f is Subfield of Image g
set If = Image f;
set Ig = Image g;
H1: ( rng f = the carrier of (Image f) & rng g = the carrier of (Image g) ) by RING_2:def 6;
F is Subfield of E by FIELD_4:7;
then H3: the carrier of F c= the carrier of E by EC_PF_1:def 1;
A: the carrier of (Image f) c= the carrier of (Image g)

proof

now :: thesis: for o being object st o in the carrier of (Image f) holds
o in the carrier of (Image g)

let o be object ; :: thesis: ( o in the carrier of (Image f) implies o in the carrier of (Image g) )
assume o in the carrier of (Image f) ; :: thesis: o in the carrier of (Image g)
then consider u being object such that
A1: ( u in dom f & f . u = o ) by H1, FUNCT_1:def 3;
reconsider a = u as Element of F by A1;
reconsider a1 = a as Element of E by H3;
A2: dom g = the carrier of E by FUNCT_2:def 1;
g . a1 = o by AS, A1;
hence o in the carrier of (Image g) by H1, A2, FUNCT_1:def 3; :: thesis: verum

end;

hence the carrier of (Image f) c= the carrier of (Image g) ; :: thesis: verum

end;

H4: [: the carrier of (Image f), the carrier of (Image f):] c= [: the carrier of (Image g), the carrier of (Image g):] by A, ZFMISC_1:96;
B: the addF of (Image f) = the addF of L || the carrier of (Image f) by EC_PF_1:def 1
.= ( the addF of L || the carrier of (Image g)) || the carrier of (Image f) by H4, FUNCT_1:51
.= the addF of (Image g) || the carrier of (Image f) by EC_PF_1:def 1 ;
C: the multF of (Image f) = the multF of L || the carrier of (Image f) by EC_PF_1:def 1
.= ( the multF of L || the carrier of (Image g)) || the carrier of (Image f) by H4, FUNCT_1:51
.= the multF of (Image g) || the carrier of (Image f) by EC_PF_1:def 1 ;
D: 1. (Image f) = 1. L by RING_2:def 6
.= 1. (Image g) by RING_2:def 6 ;
0. (Image f) = 0. L by RING_2:def 6
.= 0. (Image g) by RING_2:def 6 ;
hence Image f is Subfield of Image g by A, B, C, D, EC_PF_1:def 1; :: thesis: verum