let F be Group; :: thesis:
let G be strict Group; :: thesis:
let g be Homomorphism of G,F; :: thesis:
assume G is cyclic ; :: thesis:
then consider a being Element of G such that
A1: G = gr {a} ;
ex f1 being Element of (Image g) st Image g = gr {f1}

g . a in Image g by GROUP_6:45;
then reconsider f = g . a as Element of (Image g) by STRUCT_0:def 5;
take f ; :: thesis:
for d being Element of (Image g) ex i being Integer st d = f |^ i

let d be Element of (Image g); :: thesis:
d in Image g by STRUCT_0:def 5;
then consider b being Element of G such that
A2: d = g . b by GROUP_6:45;
b in gr {a} by A1, STRUCT_0:def 5;
then consider i being Integer such that
A3: b = a |^ i by GR_CY_1:5;
take i ; :: thesis:
d = (g . a) |^ i by A2, A3, GROUP_6:37
.= f |^ i by GROUP_4:2 ;
hence d = f |^ i ; :: thesis:

end;

end;