theorem Th1: :: RINGDER1:1

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) + (n * b) = n * (a + b)