let m, n be Nat; :: thesis: for G being addGroup
for g, h being Element of G st g + h = h + g holds
(n * g) + (m * h) = (m * h) + (n * g)
let G be addGroup; :: thesis: for g, h being Element of G st g + h = h + g holds
(n * g) + (m * h) = (m * h) + (n * g)
let g, h be Element of G; :: thesis: ( g + h = h + g implies (n * g) + (m * h) = (m * h) + (n * g) )
defpred S₁[ Nat] means for m being Nat st g + h = h + g holds
($1 * g) + (m * h) = (m * h) + ($1 * 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: for m being Nat st g + h = h + g holds
(n * g) + (m * h) = (m * h) + (n * g) ; :: thesis: S₁[n + 1]
let m be Nat; :: thesis: ( g + h = h + g implies ((n + 1) * g) + (m * h) = (m * h) + ((n + 1) * g) )
assume A3: g + h = h + g ; :: thesis: ((n + 1) * g) + (m * h) = (m * h) + ((n + 1) * g)
thus ((n + 1) * g) + (m * h) = (g + (n * g)) + (m * h) by Lm6
.= g + ((n * g) + (m * h)) by RLVECT_1:def 3
.= g + ((m * h) + (n * g)) by A2, A3
.= (g + (m * h)) + (n * g) by RLVECT_1:def 3
.= ((m * h) + g) + (n * g) by A3, Lm9
.= (m * h) + (g + (n * g)) by RLVECT_1:def 3
.= (m * h) + ((n + 1) * g) by Lm6 ; :: thesis: verum

end;

A4: S₁[ 0 ]

proof

let m be Nat; :: thesis: ( g + h = h + g implies (0 * g) + (m * h) = (m * h) + (0 * g) )
assume g + h = h + g ; :: thesis: (0 * g) + (m * h) = (m * h) + (0 * g)
thus (0 * g) + (m * h) = (0_ G) + (m * h) by Def7
.= m * h by Def4
.= (m * h) + (0_ G) by Def4
.= (m * h) + (0 * 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 (n * g) + (m * h) = (m * h) + (n * g) ) ; :: thesis: verum