set F = R;
set E = S;
X: R is Subring of S by FIELD_4:def 1;
set g = hom_Ext_eval (a,R);

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

let x, y be Element of (Polynom-Ring R); :: thesis: (hom_Ext_eval (a,R)) . (x + y) = ((hom_Ext_eval (a,R)) . x) + ((hom_Ext_eval (a,R)) . y)
reconsider p = x, q = y as Polynomial of R by POLYNOM3:def 10;
thus (hom_Ext_eval (a,R)) . (x + y) = (hom_Ext_eval (a,R)) . (p + q) by POLYNOM3:def 10
.= Ext_eval ((p + q),a) by ALGNUM_1:def 11
.= (Ext_eval (p,a)) + (Ext_eval (q,a)) by X, ALGNUM_1:15
.= ((hom_Ext_eval (a,R)) . x) + (Ext_eval (q,a)) by ALGNUM_1:def 11
.= ((hom_Ext_eval (a,R)) . x) + ((hom_Ext_eval (a,R)) . y) by ALGNUM_1:def 11 ; :: thesis: verum

end;

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

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

let x, y be Element of (Polynom-Ring R); :: thesis: (hom_Ext_eval (a,R)) . (x * y) = ((hom_Ext_eval (a,R)) . x) * ((hom_Ext_eval (a,R)) . y)
reconsider p = x, q = y as Polynomial of R by POLYNOM3:def 10;
thus (hom_Ext_eval (a,R)) . (x * y) = (hom_Ext_eval (a,R)) . (p *' q) by POLYNOM3:def 10
.= Ext_eval ((p *' q),a) by ALGNUM_1:def 11
.= (Ext_eval (p,a)) * (Ext_eval (q,a)) by X, ALGNUM_1:20
.= ((hom_Ext_eval (a,R)) . x) * (Ext_eval (q,a)) by ALGNUM_1:def 11
.= ((hom_Ext_eval (a,R)) . x) * ((hom_Ext_eval (a,R)) . y) by ALGNUM_1:def 11 ; :: thesis: verum

end;

hence hom_Ext_eval (a,R) is multiplicative ; :: thesis: hom_Ext_eval (a,R) is unity-preserving
(hom_Ext_eval (a,R)) . (1_ (Polynom-Ring R)) = (hom_Ext_eval (a,R)) . (1_. R) by POLYNOM3:37
.= Ext_eval ((1_. R),a) by ALGNUM_1:def 11
.= 1_ S by X, ALGNUM_1:14 ;
hence hom_Ext_eval (a,R) is unity-preserving ; :: thesis: verum