let n be 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 )
defpred S₁[ Nat] means a |^ $1 in H;
assume A1: a in H ; :: thesis: a |^ n in H

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] )
A3: a |^ (n + 1) = (a |^ n) * a by GROUP_1:34;
assume S₁[n] ; :: thesis: S₁[n + 1]
hence S₁[n + 1] by A1, A3, GROUP_2:50; :: thesis: verum

end;

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