theorem c1: :: REALALG2:5

for R being non empty right_complementable Abelian add-associative right_zeroed left-distributive doubleLoopStr
for a, b being Element of R
for i being Integer holds i '*' (a * b) = (i '*' a) * b