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

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