theorem Th21: :: ALGNUM_1:17

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