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