let G, F be strict Group; :: thesis: ( G,F are_isomorphic & G is cyclic implies F is cyclic )

assume that

A1: G,F are_isomorphic and

A2: G is cyclic ; :: thesis: F is cyclic

consider h being Homomorphism of G,F such that

A3: h is bijective by A1, GROUP_6:def 11;

h is onto by A3, FUNCT_2:def 4;

then Image h = F by GROUP_6:57;

hence F is cyclic by A2, Th26; :: thesis: verum

assume that

A1: G,F are_isomorphic and

A2: G is cyclic ; :: thesis: F is cyclic

consider h being Homomorphism of G,F such that

A3: h is bijective by A1, GROUP_6:def 11;

h is onto by A3, FUNCT_2:def 4;

then Image h = F by GROUP_6:57;

hence F is cyclic by A2, Th26; :: thesis: verum