theorem Th3: :: RINGDER1:3

for L being non empty right_complementable associative Abelian add-associative right_zeroed distributive left_zeroed doubleLoopStr
for n being Nat holds n * (0. L) = 0. L