let G, H be Group; :: thesis: for h being Homomorphism of G,H st h is one-to-one holds
G, Image h are_isomorphic
let h be Homomorphism of G,H; :: thesis: ( h is one-to-one implies G, Image h are_isomorphic )
reconsider ih = h as Homomorphism of G,(Image h) by Th49;
assume A1: h is one-to-one ; :: thesis: G, Image h are_isomorphic
take ih ; :: according to GROUP_6:def 11 :: thesis: ih is bijective
ih is onto by Th44;
hence ih is bijective by A1; :: thesis: verum