let m, n be Nat; :: thesis: for G being Group
for h being Element of G holds h |^ (n + m) = (h |^ n) * (h |^ m)
let G be Group; :: thesis: for h being Element of G holds h |^ (n + m) = (h |^ n) * (h |^ m)
let h be Element of G; :: thesis: h |^ (n + m) = (h |^ n) * (h |^ m)
defpred S₁[ Nat] means for n being Nat holds h |^ (n + $1) = (h |^ n) * (h |^ $1);
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 h |^ (n + m) = (h |^ n) * (h |^ m) ; :: thesis: S₁[m + 1]
let n be Nat; :: thesis: h |^ (n + (m + 1)) = (h |^ n) * (h |^ (m + 1))
thus h |^ (n + (m + 1)) = h |^ ((n + m) + 1)
.= (h |^ (n + m)) * h by Lm2
.= ((h |^ n) * (h |^ m)) * h by A2
.= (h |^ n) * ((h |^ m) * h) by Def3
.= (h |^ n) * (h |^ (m + 1)) by Lm2 ; :: thesis: verum

end;

A3: S₁[ 0 ]

proof

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

end;

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