let G be Group; :: thesis: for h being Element of G
for n being Nat holds
( h |^ (n + 1) = (h |^ n) * h & h |^ (n + 1) = h * (h |^ n) )
let h be Element of G; :: thesis: for n being Nat holds
( h |^ (n + 1) = (h |^ n) * h & h |^ (n + 1) = h * (h |^ n) )
let n be Nat; :: 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 Th48
.= h * (h |^ n) by Th44 ; :: thesis: verum