let n be Element of 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 )
assume A1: a = h ; :: thesis: a |^ n = h |^ n
defpred S₁[ Element of NAT ] means a |^ $1 = h |^ $1;
a |^ 0 = 1_ G by GROUP_1:43
.= 1_ H by GROUP_2:53
.= h |^ 0 by GROUP_1:43 ;
then A2: S₁[ 0 ] ;

A3: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
a |^ (n + 1) = (a |^ n) * a by GROUP_1:66
.= (h |^ n) * h by A1, A4, GROUP_2:52
.= h |^ (n + 1) by GROUP_1:66 ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A3);
hence a |^ n = h |^ n ; :: thesis: verum