let R be Ring; :: thesis: for S being RingExtension of R

for a being Element of S

for p, q being Polynomial of R holds Ext_eval ((p + q),a) = (Ext_eval (p,a)) + (Ext_eval (q,a))

let S be RingExtension of R; :: thesis: for a being Element of S

for p, q being Polynomial of R holds Ext_eval ((p + q),a) = (Ext_eval (p,a)) + (Ext_eval (q,a))

let a be Element of S; :: thesis: for p, q being Polynomial of R holds Ext_eval ((p + q),a) = (Ext_eval (p,a)) + (Ext_eval (q,a))

let p, q be Polynomial of R; :: thesis: Ext_eval ((p + q),a) = (Ext_eval (p,a)) + (Ext_eval (q,a))

R is Subring of S by Def1;

hence Ext_eval ((p + q),a) = (Ext_eval (p,a)) + (Ext_eval (q,a)) by ALGNUM_1:15; :: thesis: verum

for a being Element of S

for p, q being Polynomial of R holds Ext_eval ((p + q),a) = (Ext_eval (p,a)) + (Ext_eval (q,a))

let S be RingExtension of R; :: thesis: for a being Element of S

for p, q being Polynomial of R holds Ext_eval ((p + q),a) = (Ext_eval (p,a)) + (Ext_eval (q,a))

let a be Element of S; :: thesis: for p, q being Polynomial of R holds Ext_eval ((p + q),a) = (Ext_eval (p,a)) + (Ext_eval (q,a))

let p, q be Polynomial of R; :: thesis: Ext_eval ((p + q),a) = (Ext_eval (p,a)) + (Ext_eval (q,a))

R is Subring of S by Def1;

hence Ext_eval ((p + q),a) = (Ext_eval (p,a)) + (Ext_eval (q,a)) by ALGNUM_1:15; :: thesis: verum