for A being Ring
for B being comRing
for p, q being Polynomial of A
for x being Element of B st A is Subring of B holds
Ext_eval (((Leading-Monomial p) *' q),x) = (Ext_eval ((Leading-Monomial p),x)) * (Ext_eval (q,x))