theorem :: ALGSTR_2:9

for G being left-distributive doubleLoop
for a, x, y being Element of G holds (x - y) * a = (x * a) - (y * a)