theorem Th23: :: POLYNOM1:23

for n being set
for L being non empty right_zeroed addLoopStr
for p being Series of n,L holds p + (0_ (n,L)) = p