set g = hom_Ext_eval (x,R);
H: R is Subring of S by FIELD_4:def 1;

now :: thesis: for x1, x2 being Element of (Polynom-Ring (n,R)) holds (hom_Ext_eval (x,R)) . (x1 + x2) = ((hom_Ext_eval (x,R)) . x1) + ((hom_Ext_eval (x,R)) . x2)

let x1, x2 be Element of (Polynom-Ring (n,R)); :: thesis: (hom_Ext_eval (x,R)) . (x1 + x2) = ((hom_Ext_eval (x,R)) . x1) + ((hom_Ext_eval (x,R)) . x2)
reconsider p = x1, q = x2 as Polynomial of n,R by POLYNOM1:def 11;
thus (hom_Ext_eval (x,R)) . (x1 + x2) = (hom_Ext_eval (x,R)) . (p + q) by POLYNOM1:def 11
.= Ext_eval ((p + q),x) by dh
.= (Ext_eval (p,x)) + (Ext_eval (q,x)) by H, FIELD_11:19
.= ((hom_Ext_eval (x,R)) . x1) + (Ext_eval (q,x)) by dh
.= ((hom_Ext_eval (x,R)) . x1) + ((hom_Ext_eval (x,R)) . x2) by dh ; :: thesis: verum

end;

hence hom_Ext_eval (x,R) is additive ; :: thesis: ( hom_Ext_eval (x,R) is multiplicative & hom_Ext_eval (x,R) is unity-preserving )

now :: thesis: for x1, x2 being Element of (Polynom-Ring (n,R)) holds (hom_Ext_eval (x,R)) . (x1 * x2) = ((hom_Ext_eval (x,R)) . x1) * ((hom_Ext_eval (x,R)) . x2)

let x1, x2 be Element of (Polynom-Ring (n,R)); :: thesis: (hom_Ext_eval (x,R)) . (x1 * x2) = ((hom_Ext_eval (x,R)) . x1) * ((hom_Ext_eval (x,R)) . x2)
reconsider p = x1, q = x2 as Polynomial of n,R by POLYNOM1:def 11;
thus (hom_Ext_eval (x,R)) . (x1 * x2) = (hom_Ext_eval (x,R)) . (p *' q) by POLYNOM1:def 11
.= Ext_eval ((p *' q),x) by dh
.= (Ext_eval (p,x)) * (Ext_eval (q,x)) by H, FIELD_11:20
.= ((hom_Ext_eval (x,R)) . x1) * (Ext_eval (q,x)) by dh
.= ((hom_Ext_eval (x,R)) . x1) * ((hom_Ext_eval (x,R)) . x2) by dh ; :: thesis: verum

end;

hence hom_Ext_eval (x,R) is multiplicative ; :: thesis: hom_Ext_eval (x,R) is unity-preserving
(hom_Ext_eval (x,R)) . (1_ (Polynom-Ring (n,R))) = (hom_Ext_eval (x,R)) . (1_ (n,R)) by POLYNOM1:def 11
.= Ext_eval ((1_ (n,R)),x) by dh
.= 1_ S by H, FIELD_11:17 ;
hence hom_Ext_eval (x,R) is unity-preserving ; :: thesis: verum