theorem evalti: :: FIELD_11:20

for R, S being non degenerated comRing
for n being Ordinal
for p, q being Polynomial of n,R
for x being Function of n,S st R is Subring of S holds
Ext_eval ((p *' q),x) = (Ext_eval (p,x)) * (Ext_eval (q,x))