theorem Th24: :: POLYNOM5:24

for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for p being Polynomial of L holds len ((0. L) * p) = 0