let n be Nat; :: thesis: for G being Group
for a being Element of G
for H being Subgroup of G
for h being Element of H st a = h holds
a |^ n = h |^ n
let G be Group; :: thesis: for a being Element of G
for H being Subgroup of G
for h being Element of H st a = h holds
a |^ n = h |^ n
let a be Element of G; :: thesis: for H being Subgroup of G
for h being Element of H st a = h holds
a |^ n = h |^ n
let H be Subgroup of G; :: thesis: for h being Element of H st a = h holds
a |^ n = h |^ n
let h be Element of H; :: thesis: ( a = h implies a |^ n = h |^ n )
defpred S₁[ Nat] means a |^ $1 = h |^ $1;
assume A1: a = h ; :: thesis: a |^ n = h |^ n

A2: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
a |^ (n + 1) = (a |^ n) * a by GROUP_1:34
.= (h |^ n) * h by A1, A3, GROUP_2:43
.= h |^ (n + 1) by GROUP_1:34 ;
hence S₁[n + 1] ; :: thesis: verum

end;

a |^ 0 = 1_ G by GROUP_1:25
.= 1_ H by GROUP_2:44
.= h |^ 0 by GROUP_1:25 ;
then A4: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A2);
hence a |^ n = h |^ n ; :: thesis: verum