theorem Th26: :: POLYNOM3:28

for L being non empty right_zeroed addLoopStr
for p being sequence of L holds p + (0_. L) = p