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_{1}( 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_{1}(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

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

consider f being FinSequence such that

A3: ( len f = ord b & ( for i being Nat st i in dom f holds

f . i = H

A4: dom f = Seg (ord b) by A3, FINSEQ_1:def 3;

the carrier of (gr {b}) c= rng f

proof

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

end;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 )
;

end;