let n be Nat; :: thesis: for G being Group
for h being Element of G st h |^ n = 1_ G holds
ord h divides n
let G be Group; :: thesis: for h being Element of G st h |^ n = 1_ G holds
ord h divides n
let h be Element of G; :: thesis: ( h |^ n = 1_ G implies ord h divides n )
defpred S₁[ Nat] means ( h |^ $1 = 1_ G implies ord h divides $1 );
A1: for n being Nat st ( for k being Nat st k < n holds
S₁[k] ) holds
S₁[n]

proof

let n be Nat; :: thesis: ( ( for k being Nat st k < n holds
S₁[k] ) implies S₁[n] )
assume A2: for k being Nat st k < n holds
S₁[k] ; :: thesis: S₁[n]
assume A3: h |^ n = 1_ G ; :: thesis: ord h divides n

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: ord h divides n

hence ord h divides n by NAT_D:6; :: thesis: verum

end;

suppose A4: n <> 0 ; :: thesis: ord h divides n

per cases ( ord h = 0 or ord h <> 0 ) ;

suppose ord h = 0 ; :: thesis: ord h divides n

then h is being_of_order_0 by Def11;
hence ord h divides n by A3, A4; :: thesis: verum

end;

suppose A5: ord h <> 0 ; :: thesis: ord h divides n

then not h is being_of_order_0 by Def11;
then ord h <= n by A3, A4, Def11;
then consider m being Nat such that
A6: n = (ord h) + m by NAT_1:10;
h |^ n = (h |^ (ord h)) * (h |^ m) by A6, Lm5
.= (1_ G) * (h |^ m) by Th40
.= h |^ m by Def4 ;
then ord h divides m by A2, A3, A5, A6, NAT_1:16;
then consider i being Nat such that
A7: m = (ord h) * i by NAT_D:def 3;
n = (ord h) * (1 + i) by A6, A7;
hence ord h divides n by NAT_D:def 3; :: thesis: verum

end;

end;

end;

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 4(A1);
hence ( h |^ n = 1_ G implies ord h divides n ) ; :: thesis: verum