theorem :: ALGSTR_2:5

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