theorem Th22: :: ALGNUM_1:18

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) *' (Leading-Monomial q)),x) = (Ext_eval ((Leading-Monomial p),x)) * (Ext_eval ((Leading-Monomial q),x))