let n be Nat; :: thesis: for F being Field
for E being FieldExtension of F
for x being Function of n,E
for a, b being Element of (Image_hom_Ext_eval (x,F))
for x1, x2 being Element of E st a = x1 & b = x2 holds
( a + b = x1 + x2 & a * b = x1 * x2 )
let F be Field; :: thesis: for E being FieldExtension of F
for x being Function of n,E
for a, b being Element of (Image_hom_Ext_eval (x,F))
for x1, x2 being Element of E st a = x1 & b = x2 holds
( a + b = x1 + x2 & a * b = x1 * x2 )
let E be FieldExtension of F; :: thesis: for x being Function of n,E
for a, b being Element of (Image_hom_Ext_eval (x,F))
for x1, x2 being Element of E st a = x1 & b = x2 holds
( a + b = x1 + x2 & a * b = x1 * x2 )
let x be Function of n,E; :: thesis: for a, b being Element of (Image_hom_Ext_eval (x,F))
for x1, x2 being Element of E st a = x1 & b = x2 holds
( a + b = x1 + x2 & a * b = x1 * x2 )
let a, b be Element of (Image_hom_Ext_eval (x,F)); :: thesis: for x1, x2 being Element of E st a = x1 & b = x2 holds
( a + b = x1 + x2 & a * b = x1 * x2 )
let x1, x2 be Element of E; :: thesis: ( a = x1 & b = x2 implies ( a + b = x1 + x2 & a * b = x1 * x2 ) )
set I = Image_hom_Ext_eval (x,F);
set f = hom_Ext_eval (x,F);
the carrier of (Image_hom_Ext_eval (x,F)) = rng (hom_Ext_eval (x,F)) by defIm;
then A1: [a,b] in [:(rng (hom_Ext_eval (x,F))),(rng (hom_Ext_eval (x,F))):] ;
assume AS: ( a = x1 & b = x2 ) ; :: thesis: ( a + b = x1 + x2 & a * b = x1 * x2 )
the addF of (Image_hom_Ext_eval (x,F)) . (a,b) = ( the addF of E || (rng (hom_Ext_eval (x,F)))) . (a,b) by defIm
.= the addF of E . (x1,x2) by AS, A1, FUNCT_1:49 ;
hence a + b = x1 + x2 ; :: thesis: a * b = x1 * x2
the multF of (Image_hom_Ext_eval (x,F)) . (a,b) = ( the multF of E || (rng (hom_Ext_eval (x,F)))) . (a,b) by defIm
.= the multF of E . (x1,x2) by AS, A1, FUNCT_1:49 ;
hence a * b = x1 * x2 ; :: thesis: verum