let n be Nat; :: thesis: for F being Field
for E being FieldExtension of F
for x being Function of n,E holds F is Subring of Image_hom_Ext_eval (x,F)
let F be Field; :: thesis: for E being FieldExtension of F
for x being Function of n,E holds F is Subring of Image_hom_Ext_eval (x,F)
let E be FieldExtension of F; :: thesis: for x being Function of n,E holds F is Subring of Image_hom_Ext_eval (x,F)
let x be Function of n,E; :: thesis: F is Subring of Image_hom_Ext_eval (x,F)
set R = Image_hom_Ext_eval (x,F);
set f = hom_Ext_eval (x,F);
U: F is Subring of E by FIELD_4:def 1;
then Y: the carrier of F c= the carrier of E by C0SP1:def 3;

Z: now :: thesis: for o being object st o in the carrier of F holds
o in rng (hom_Ext_eval (x,F))

let o be object ; :: thesis: ( o in the carrier of F implies o in rng (hom_Ext_eval (x,F)) )
assume o in the carrier of F ; :: thesis: o in rng (hom_Ext_eval (x,F))
then reconsider b = o as Element of F ;
reconsider c = b as Element of E by Y;
reconsider p = b | (n,F) as Element of the carrier of (Polynom-Ring (n,F)) by POLYNOM1:def 11;
reconsider q = c | (n,E) as Element of the carrier of (Polynom-Ring (n,E)) by POLYNOM1:def 11;
Ext_eval ((b | (n,F)),x) = eval ((c | (n,E)),x) by field427, field426
.= b by POLYNOM7:25 ;
then b in { (Ext_eval (p,x)) where p is Polynomial of n,F : verum } ;
hence o in rng (hom_Ext_eval (x,F)) by lemphi1; :: thesis: verum

end;

then ZZ: the carrier of F c= rng (hom_Ext_eval (x,F)) ;

now :: thesis: for o being object st o in the carrier of F holds
o in the carrier of (Image_hom_Ext_eval (x,F))

let o be object ; :: thesis: ( o in the carrier of F implies o in the carrier of (Image_hom_Ext_eval (x,F)) )
assume o in the carrier of F ; :: thesis: o in the carrier of (Image_hom_Ext_eval (x,F))
then o in rng (hom_Ext_eval (x,F)) by Z;
hence o in the carrier of (Image_hom_Ext_eval (x,F)) by defIm; :: thesis: verum

end;

then A: the carrier of F c= the carrier of (Image_hom_Ext_eval (x,F)) ;
set adF = the addF of F;
set adR = the addF of (Image_hom_Ext_eval (x,F));
H1c: dom the addF of E = [: the carrier of E, the carrier of E:] by FUNCT_2:def 1;
the addF of (Image_hom_Ext_eval (x,F)) = the addF of E || (rng (hom_Ext_eval (x,F))) by defIm
.= the addF of E | [:(rng (hom_Ext_eval (x,F))),(rng (hom_Ext_eval (x,F))):] ;
then H1b: dom the addF of (Image_hom_Ext_eval (x,F)) = [: the carrier of E, the carrier of E:] /\ [:(rng (hom_Ext_eval (x,F))),(rng (hom_Ext_eval (x,F))):] by H1c, RELAT_1:61;
H1: dom ( the addF of (Image_hom_Ext_eval (x,F)) || the carrier of F) = (dom the addF of (Image_hom_Ext_eval (x,F))) /\ [: the carrier of F, the carrier of F:] by RELAT_1:61
.= [: the carrier of E, the carrier of E:] /\ ([:(rng (hom_Ext_eval (x,F))),(rng (hom_Ext_eval (x,F))):] /\ [: the carrier of F, the carrier of F:]) by H1b, XBOOLE_1:16
.= [: the carrier of E, the carrier of E:] /\ [: the carrier of F, the carrier of F:] by ZZ, ZFMISC_1:96, XBOOLE_1:28
.= [: the carrier of F, the carrier of F:] by Y, ZFMISC_1:96, XBOOLE_1:28
.= dom the addF of F by FUNCT_2:def 1 ;

now :: thesis: for o being object st o in dom the addF of F holds
the addF of F . o = ( the addF of (Image_hom_Ext_eval (x,F)) | [: the carrier of F, the carrier of F:]) . o

let o be object ; :: thesis: ( o in dom the addF of F implies the addF of F . o = ( the addF of (Image_hom_Ext_eval (x,F)) | [: the carrier of F, the carrier of F:]) . o )
assume AS: o in dom the addF of F ; :: thesis: the addF of F . o = ( the addF of (Image_hom_Ext_eval (x,F)) | [: the carrier of F, the carrier of F:]) . o
then consider a, b being object such that
B1: ( a in the carrier of F & b in the carrier of F & o = [a,b] ) by ZFMISC_1:def 2;
reconsider a = a, b = b as Element of F by B1;
( a in rng (hom_Ext_eval (x,F)) & b in rng (hom_Ext_eval (x,F)) ) by Z;
then B3: o in [:(rng (hom_Ext_eval (x,F))),(rng (hom_Ext_eval (x,F))):] by B1, ZFMISC_1:def 2;
B5: the addF of F = the addF of E || the carrier of F by C0SP1:def 3, U;
thus the addF of F . o = the addF of E . o by AS, B5, FUNCT_1:49
.= ( the addF of E || (rng (hom_Ext_eval (x,F)))) . o by B3, FUNCT_1:49
.= the addF of (Image_hom_Ext_eval (x,F)) . o by defIm
.= ( the addF of (Image_hom_Ext_eval (x,F)) | [: the carrier of F, the carrier of F:]) . o by AS, H1, FUNCT_1:47 ; :: thesis: verum

end;

then B: the addF of F = the addF of (Image_hom_Ext_eval (x,F)) || the carrier of F by H1;
set muF = the multF of F;
set muR = the multF of (Image_hom_Ext_eval (x,F));
H1c: dom the multF of E = [: the carrier of E, the carrier of E:] by FUNCT_2:def 1;
the multF of (Image_hom_Ext_eval (x,F)) = the multF of E || (rng (hom_Ext_eval (x,F))) by defIm
.= the multF of E | [:(rng (hom_Ext_eval (x,F))),(rng (hom_Ext_eval (x,F))):] ;
then H1b: dom the multF of (Image_hom_Ext_eval (x,F)) = [: the carrier of E, the carrier of E:] /\ [:(rng (hom_Ext_eval (x,F))),(rng (hom_Ext_eval (x,F))):] by H1c, RELAT_1:61;
H1: dom ( the multF of (Image_hom_Ext_eval (x,F)) || the carrier of F) = (dom the multF of (Image_hom_Ext_eval (x,F))) /\ [: the carrier of F, the carrier of F:] by RELAT_1:61
.= [: the carrier of E, the carrier of E:] /\ ([:(rng (hom_Ext_eval (x,F))),(rng (hom_Ext_eval (x,F))):] /\ [: the carrier of F, the carrier of F:]) by H1b, XBOOLE_1:16
.= [: the carrier of E, the carrier of E:] /\ [: the carrier of F, the carrier of F:] by ZZ, ZFMISC_1:96, XBOOLE_1:28
.= [: the carrier of F, the carrier of F:] by Y, ZFMISC_1:96, XBOOLE_1:28
.= dom the multF of F by FUNCT_2:def 1 ;

now :: thesis: for o being object st o in dom the multF of F holds
the multF of F . o = ( the multF of (Image_hom_Ext_eval (x,F)) | [: the carrier of F, the carrier of F:]) . o

let o be object ; :: thesis: ( o in dom the multF of F implies the multF of F . o = ( the multF of (Image_hom_Ext_eval (x,F)) | [: the carrier of F, the carrier of F:]) . o )
assume AS: o in dom the multF of F ; :: thesis: the multF of F . o = ( the multF of (Image_hom_Ext_eval (x,F)) | [: the carrier of F, the carrier of F:]) . o
then consider a, b being object such that
B1: ( a in the carrier of F & b in the carrier of F & o = [a,b] ) by ZFMISC_1:def 2;
reconsider a = a, b = b as Element of F by B1;
( a in rng (hom_Ext_eval (x,F)) & b in rng (hom_Ext_eval (x,F)) ) by Z;
then B3: o in [:(rng (hom_Ext_eval (x,F))),(rng (hom_Ext_eval (x,F))):] by B1, ZFMISC_1:def 2;
B5: the multF of F = the multF of E || the carrier of F by C0SP1:def 3, U;
thus the multF of F . o = the multF of E . o by AS, B5, FUNCT_1:49
.= ( the multF of E || (rng (hom_Ext_eval (x,F)))) . o by B3, FUNCT_1:49
.= the multF of (Image_hom_Ext_eval (x,F)) . o by defIm
.= ( the multF of (Image_hom_Ext_eval (x,F)) | [: the carrier of F, the carrier of F:]) . o by AS, H1, FUNCT_1:47 ; :: thesis: verum

end;

then C: the multF of F = the multF of (Image_hom_Ext_eval (x,F)) || the carrier of F by H1;
D: 0. F = 0. E by U, C0SP1:def 3
.= 0. (Image_hom_Ext_eval (x,F)) by defIm ;
1. F = 1. E by U, C0SP1:def 3
.= 1. (Image_hom_Ext_eval (x,F)) by defIm ;
hence F is Subring of Image_hom_Ext_eval (x,F) by A, B, C, D, C0SP1:def 3; :: thesis: verum