theorem Th8: :: POLYRED:8

for X being set
for L being non empty left_add-cancelable left-distributive right_zeroed doubleLoopStr
for p being Series of X,L holds (0. L) * p = 0_ (X,L)