for G being addGroup
for a, b being Element of G
for n being Nat holds (n * a) * b = n * (a * b) by Lm4;