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 A4: dom f = Seg (ord b) by ;
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 ;
set k = m mod (ord b);
reconsider k = m mod (ord b) as Element of NAT by ;
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 ;
then A9: ord b in Seg (ord b) by FINSEQ_1:1;
a = 1_ G by
.= b |^ (ord b) by
.= f . (ord b) by A3, A4, A9 ;
hence x in rng f by ; :: thesis: verum
end;
suppose A10: k <> 0 ; :: thesis: x in rng f
A11: k < ord b by ;
k >= 0 + 1 by ;
then A12: k in Seg (ord b) by ;
then a = f . k by A3, A4, A7;
hence x in rng f by ; :: thesis: verum
end;
end;
end;
hence the carrier of (gr {b}) is finite ; :: according to STRUCT_0:def 11 :: thesis: verum