theorem :: RINGDER1:2

for L being non empty right_complementable associative Abelian add-associative right_zeroed distributive left_zeroed doubleLoopStr
for a, b being Element of L
for n being Nat holds (n * a) * b = a * (n * b)