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} ;
ex f1 being Element of (Image g) st Image g = gr {f1}

proof

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: Image g = gr {f}
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
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 = f |^ i
d = (g . a) |^ i by A2, A3, GROUP_6:37
.= f |^ i by GROUP_4:2 ;
hence d = f |^ i ; :: thesis: verum

end;

hence Image g = gr {f} by Th5; :: thesis: verum

end;

hence Image g is cyclic ; :: thesis: verum