theorem Th20: :: ALGNUM_1:16

for A, B being Ring
for p, q being Polynomial of A st A is Subring of B & len p > 0 & len q > 0 holds
for x being Element of B holds Ext_eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (In (((p . ((len p) -' 1)) * (q . ((len q) -' 1))),B)) * ((power B) . (x,(((len p) + (len q)) -' 2)))