let n be Nat; :: thesis: for G being addGroup
for g, h being Element of G st g + h = h + g holds
g + (n * h) = (n * h) + g
let G be addGroup; :: thesis: for g, h being Element of G st g + h = h + g holds
g + (n * h) = (n * h) + g
let g, h be Element of G; :: thesis: ( g + h = h + g implies g + (n * h) = (n * h) + g )
defpred S₁[ Nat] means ( g + h = h + g implies g + ($1 * h) = ($1 * h) + g );
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: ( g + h = h + g implies g + (n * h) = (n * h) + g ) ; :: thesis: S₁[n + 1]
assume A3: g + h = h + g ; :: thesis: g + ((n + 1) * h) = ((n + 1) * h) + g
thus g + ((n + 1) * h) = g + (h + (n * h)) by Lm6
.= (g + h) + (n * h) by RLVECT_1:def 3
.= h + ((n * h) + g) by A2, A3, RLVECT_1:def 3
.= (h + (n * h)) + g by RLVECT_1:def 3
.= ((n + 1) * h) + g by Lm6 ; :: thesis: verum

end;

A4: S₁[ 0 ]

proof

assume g + h = h + g ; :: thesis: g + (0 * h) = (0 * h) + g
thus g + (0 * h) = g + (0_ G) by Def7
.= g by Def4
.= (0_ G) + g by Def4
.= (0 * h) + g by Def7 ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A1);
hence ( g + h = h + g implies g + (n * h) = (n * h) + g ) ; :: thesis: verum