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