theorem :: FIELD_4:25

for R being comRing
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))