theorem Th11: :: FIELD_11:18

for R, S being non degenerated comRing
for n being Ordinal
for p being Polynomial of n,R
for b being bag of n st Support p = {b} holds
for x being Function of n,S holds Ext_eval (p,x) = (In ((p . b),S)) * (eval (b,x))