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 H1( 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 = H1(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;
end;
end;
hence the carrier of (gr {b}) is finite ; :: according to STRUCT_0:def 11 :: thesis: verum