theorem evalpl: :: FIELD_11:19

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))