theorem Th2: :: POLYRED:2

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