let i be Integer; :: thesis: for G being Group
for h being Element of G holds
( h |^ (i + 1) = (h |^ i) * h & h |^ (i + 1) = h * (h |^ i) )
let G be Group; :: thesis: for h being Element of G holds
( h |^ (i + 1) = (h |^ i) * h & h |^ (i + 1) = h * (h |^ i) )
let h be Element of G; :: thesis: ( h |^ (i + 1) = (h |^ i) * h & h |^ (i + 1) = h * (h |^ i) )
h |^ 1 = h by Th25;
hence ( h |^ (i + 1) = (h |^ i) * h & h |^ (i + 1) = h * (h |^ i) ) by Th32; :: thesis: verum