let R be comRing; :: thesis: for S being comRingExtension 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 comRingExtension 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:20; :: thesis: verum