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

proof

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

proof

let d be Element of (Image g); :: thesis: ex i being Integer st d = f |^ i
d in Image g by STRUCT_0:def 5;
then consider b being Element of G such that
A3: d = g . b by GROUP_6:54;
b in gr {a} by A1, STRUCT_0:def 5;
then consider i being Integer such that
A4: b = a |^ i by GR_CY_1:25;
A5: d = (g . a) |^ i by A3, A4, GROUP_6:46
.= f |^ i by GROUP_4:4 ;
take i ; :: thesis: d = f |^ i
thus d = f |^ i by A5; :: thesis: verum

end;

take f ; :: thesis: Image g = gr {f}
thus Image g = gr {f} by A2, Th11; :: thesis: verum

end;

hence Image g is cyclic by GR_CY_1:def 9; :: thesis: verum