let n be Nat; :: thesis: for G being addGroup
for g, h being Element of G st g + h = h + g holds
n * (g + h) = (n * g) + (n * h)
let G be addGroup; :: thesis: for g, h being Element of G st g + h = h + g holds
n * (g + h) = (n * g) + (n * h)
let g, h be Element of G; :: thesis: ( g + h = h + g implies n * (g + h) = (n * g) + (n * h) )
defpred S1[ Nat] means ( g + h = h + g implies $1 * (g + h) = ($1 * g) + ($1 * h) );
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A2: ( g + h = h + g implies n * (g + h) = (n * g) + (n * h) ) ; :: thesis: S1[n + 1]
assume A3: g + h = h + g ; :: thesis: (n + 1) * (g + h) = ((n + 1) * g) + ((n + 1) * h)
hence (n + 1) * (g + h) = ((n * g) + (n * h)) + (h + g) by A2, Lm6
.= (((n * g) + (n * h)) + h) + g by RLVECT_1:def 3
.= ((n * g) + ((n * h) + h)) + g by RLVECT_1:def 3
.= ((n * g) + ((n + 1) * h)) + g by Lm6
.= (((n + 1) * h) + (n * g)) + g by A3, Lm10
.= ((n + 1) * h) + ((n * g) + g) by RLVECT_1:def 3
.= ((n + 1) * h) + ((n + 1) * g) by Lm6
.= ((n + 1) * g) + ((n + 1) * h) by A3, Lm10 ;
:: thesis: verum
end;
A4: S1[ 0 ]
proof
assume g + h = h + g ; :: thesis: 0 * (g + h) = (0 * g) + (0 * h)
thus 0 * (g + h) = 0_ G by Def7
.= (0_ G) + (0_ G) by Def4
.= (0 * g) + (0_ G) by Def7
.= (0 * g) + (0 * h) by Def7 ; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A4, A1);
 hence ( g + h = h + g implies n * (g + h) = (n * g) + (n * h) ) ; :: thesis: verum