defpred S₁[ Nat] means for G being addGroup
for a, b being Element of G holds ($1 * a) * b = $1 * (a * b);
A1: for k being Nat st S₁[k] holds
S₁[k + 1] by Lm3;
A2: S₁[ 0 ] by Lm2;
for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A1);
hence for n being Nat
for G being addGroup
for a, b being Element of G holds (n * a) * b = n * (a * b) ; :: thesis: verum