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 () st Image g = gr {f1}
proof
g . a in Image g by GROUP_6:45;
then reconsider f = g . a as Element of () by STRUCT_0:def 5;
take f ; :: thesis:
for d being Element of () ex i being Integer st d = f |^ i
proof
let d be Element of (); :: 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 ;
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
.= 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