let n be Element of NAT ; :: thesis: for G being Group
for a being Element of G
for H being Subgroup of G st a in H holds
a |^ n in H
let G be Group; :: thesis: for a being Element of G
for H being Subgroup of G st a in H holds
a |^ n in H
let a be Element of G; :: thesis: for H being Subgroup of G st a in H holds
a |^ n in H
let H be Subgroup of G; :: thesis: ( a in H implies a |^ n in H )
assume A1: a in H ; :: thesis: a |^ n in H
defpred S₁[ Element of NAT ] means a |^ $1 in H;
a |^ 0 = 1_ G by GROUP_1:43;
then A2: S₁[ 0 ] by GROUP_2:55;

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;
hence S₁[n + 1] by A1, A4, GROUP_2:59; :: thesis: verum

end;

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