let Gc be cyclic Group; :: thesis: for g being Element of Gc st Gc = gr {g} holds

for G being Group

for f being Homomorphism of G,Gc st g in Image f holds

f is onto

let g be Element of Gc; :: thesis: ( Gc = gr {g} implies for G being Group

for f being Homomorphism of G,Gc st g in Image f holds

f is onto )

assume A1: Gc = gr {g} ; :: thesis: for G being Group

for f being Homomorphism of G,Gc st g in Image f holds

f is onto

let G be Group; :: thesis: for f being Homomorphism of G,Gc st g in Image f holds

f is onto

let f be Homomorphism of G,Gc; :: thesis: ( g in Image f implies f is onto )

assume g in Image f ; :: thesis: f is onto

then Image f = Gc by A1, Th13;

hence f is onto by GROUP_6:57; :: thesis: verum

for G being Group

for f being Homomorphism of G,Gc st g in Image f holds

f is onto

let g be Element of Gc; :: thesis: ( Gc = gr {g} implies for G being Group

for f being Homomorphism of G,Gc st g in Image f holds

f is onto )

assume A1: Gc = gr {g} ; :: thesis: for G being Group

for f being Homomorphism of G,Gc st g in Image f holds

f is onto

let G be Group; :: thesis: for f being Homomorphism of G,Gc st g in Image f holds

f is onto

let f be Homomorphism of G,Gc; :: thesis: ( g in Image f implies f is onto )

assume g in Image f ; :: thesis: f is onto

then Image f = Gc by A1, Th13;

hence f is onto by GROUP_6:57; :: thesis: verum