let n be Nat; :: thesis: for G being Group
for h being Element of G holds h |^ (n + 1) = (h |^ n) * h
let G be Group; :: thesis: for h being Element of G holds h |^ (n + 1) = (h |^ n) * h
let h be Element of G; :: thesis: h |^ (n + 1) = (h |^ n) * h
reconsider n = n as Element of NAT by ORDINAL1:def 13;
h |^ (n + 1) = (h |^ n) * h by Def8;
hence h |^ (n + 1) = (h |^ n) * h ; :: thesis: verum