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