let n be Nat; :: thesis: for G being Group
for h being Element of G holds
( h |^ (n + 1) = (h |^ n) * h & h |^ (n + 1) = h * (h |^ n) )
let G be Group; :: thesis: for h being Element of G holds
( h |^ (n + 1) = (h |^ n) * h & h |^ (n + 1) = h * (h |^ n) )
let h be Element of G; :: thesis: ( h |^ (n + 1) = (h |^ n) * h & h |^ (n + 1) = h * (h |^ n) )
thus h |^ (n + 1) = (h |^ n) * h by Lm2; :: thesis: h |^ (n + 1) = h * (h |^ n)
thus h |^ (n + 1) = (h |^ 1) * (h |^ n) by Lm5
.= h * (h |^ n) by Th25 ; :: thesis: verum