theorem Lm30: :: ALGNUM_1:24

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