theorem Lm32: :: ALGNUM_1:26

for A being Ring
for B being comRing
for w being Element of B
for p, x being Element of (Polynom-Ring A) st A is Subring of B & x in Ann_Poly (w,A) holds
x * p in Ann_Poly (w,A)