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 S1[ Nat] means for n being Nat holds h |^ (n + $1) = (h |^ n) * (h |^ $1);
A1: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A2: for n being Nat holds h |^ (n + m) = (h |^ n) * (h |^ m) ; :: thesis: S1[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: S1[ 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 S1[m] from NAT_1:sch 2(A3, A1);
 hence h |^ (n + m) = (h |^ n) * (h |^ m) ; :: thesis: verum