let G be strict Group; :: thesis: for b being Element of G st not b is being_of_order_0 holds
gr {b} is finite
let b be Element of G; :: thesis: ( not b is being_of_order_0 implies gr {b} is finite )
assume A1: not b is being_of_order_0 ; :: thesis: gr {b} is finite
then A2: ord b <> 0 by GROUP_1:def 11;
deffunc H₁( Nat) -> Element of the carrier of G = b |^ $1;
consider f being FinSequence such that
A3: ( len f = ord b & ( for i being Nat st i in dom f holds
f . i = H₁(i) ) ) from FINSEQ_1:sch 2();
A4: dom f = Seg (ord b) by A3, FINSEQ_1:def 3;
the carrier of (gr {b}) c= rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (gr {b}) or x in rng f )
assume x in the carrier of (gr {b}) ; :: thesis: x in rng f
then A5: x in gr {b} ;
then x in G by GROUP_2:40;
then reconsider a = x as Element of G ;
consider m being Integer such that
A6: a = b |^ m by A5, GR_CY_1:5;
set k = m mod (ord b);
reconsider k = m mod (ord b) as Element of NAT by INT_1:3, NEWTON:64;
A7: a = b |^ k by A1, A6, Th10;

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

suppose A8: k = 0 ; :: thesis: x in rng f

ord b >= 0 + 1 by A2, NAT_1:13;
then A9: ord b in Seg (ord b) by FINSEQ_1:1;
a = 1_ G by A7, A8, GROUP_1:25
.= b |^ (ord b) by A1, GROUP_1:def 11
.= f . (ord b) by A3, A4, A9 ;
hence x in rng f by A4, A9, FUNCT_1:def 3; :: thesis: verum

end;

suppose A10: k <> 0 ; :: thesis: x in rng f

A11: k < ord b by A2, NEWTON:65;
k >= 0 + 1 by A10, NAT_1:13;
then A12: k in Seg (ord b) by A11, FINSEQ_1:1;
then a = f . k by A3, A4, A7;
hence x in rng f by A4, A12, FUNCT_1:def 3; :: thesis: verum

end;

end;

end;

hence the carrier of (gr {b}) is finite ; :: according to STRUCT_0:def 11 :: thesis: verum