theorem Th5: :: POLYRED:5

for n being Ordinal
for L being non empty left_add-cancelable right_complementable left-distributive add-associative right_zeroed doubleLoopStr
for p being Series of n,L holds (0_ (n,L)) *' p = 0_ (n,L)