let Gc be strict cyclic Group; :: thesis: ( Gc is infinite implies INT.Group ,Gc are_isomorphic )
consider g being Element of Gc such that
A1: for h being Element of Gc ex i being Integer st h = g |^ i by GR_CY_1:17;
assume A2: Gc is infinite ; :: thesis: INT.Group ,Gc are_isomorphic
ex h being Homomorphism of INT.Group,Gc st h is bijective

proof

deffunc H₁( Element of INT.Group) -> Element of the carrier of Gc = g |^ (@' $1);
consider h being Function of the carrier of INT.Group, the carrier of Gc such that
A3: for j1 being Element of INT.Group holds h . j1 = H₁(j1) from FUNCT_2:sch 4();
A4: Gc = gr {g} by A1, Th5;
A5: h is one-to-one

proof

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom h or not y in dom h or not h . x = h . y or x = y )
assume that
A6: x in dom h and
A7: y in dom h and
A8: h . x = h . y and
A9: x <> y ; :: thesis: contradiction
reconsider y9 = y as Element of INT.Group by A7, FUNCT_2:def 1;
reconsider x9 = x as Element of INT.Group by A6, FUNCT_2:def 1;
g |^ (@' x9) = h . y9 by A3, A8
.= g |^ (@' y9) by A3 ;
hence contradiction by A2, A4, A9, Th14; :: thesis: verum

end;

A10: dom h = the carrier of INT.Group by FUNCT_2:def 1;
A11: the carrier of Gc c= rng h

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of Gc or x in rng h )
assume x in the carrier of Gc ; :: thesis: x in rng h
then reconsider z = x as Element of Gc ;
consider i being Integer such that
A12: z = g |^ i by A1;
reconsider i9 = i as Element of INT.Group by INT_1:def 2;
i = @' i9 ;
then x = h . i9 by A3, A12;
hence x in rng h by A10, FUNCT_1:def 3; :: thesis: verum

end;

rng h c= the carrier of Gc by RELAT_1:def 19;
then A13: rng h = the carrier of Gc by A11, XBOOLE_0:def 10;
for j, j1 being Element of INT.Group holds h . (j * j1) = (h . j) * (h . j1)

proof

let j, j1 be Element of INT.Group; :: thesis: h . (j * j1) = (h . j) * (h . j1)
@' (j * j1) = (@' j) + (@' j1) ;
then h . (j * j1) = g |^ ((@' j) + (@' j1)) by A3
.= (g |^ (@' j)) * (g |^ (@' j1)) by GROUP_1:33
.= (h . j) * (g |^ (@' j1)) by A3
.= (h . j) * (h . j1) by A3 ;
hence h . (j * j1) = (h . j) * (h . j1) ; :: thesis: verum

end;

then reconsider h = h as Homomorphism of INT.Group,Gc by GROUP_6:def 6;
take h ; :: thesis: h is bijective
h is onto by A13, FUNCT_2:def 3;
hence h is bijective by A5, FUNCT_2:def 4; :: thesis: verum

end;

hence INT.Group ,Gc are_isomorphic by GROUP_6:def 11; :: thesis: verum