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

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A2: for n being Nat holds (n + m) * h = (n * h) + (m * h) ; :: thesis: S₁[m + 1]
let n be Nat; :: thesis: (n + (m + 1)) * h = (n * h) + ((m + 1) * h)
thus (n + (m + 1)) * h = ((n + m) + 1) * h
.= ((n + m) * h) + h by Def7
.= ((n * h) + (m * h)) + h by A2
.= (n * h) + ((m * h) + h) by RLVECT_1:def 3
.= (n * h) + ((m + 1) * h) by Def7 ; :: thesis: verum

end;

A3: S₁[ 0 ]

proof

let n be Nat; :: thesis: (n + 0) * h = (n * h) + (0 * h)
thus (n + 0) * h = (n * h) + (0_ G) by Def4
.= (n * h) + (0 * h) by Def7 ; :: thesis: verum

end;

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