let H, G 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 Th58;
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
the carrier of (Image h) = rng ih by Th53;
then ih is onto by FUNCT_2:def 3;
hence ih is bijective by A1; :: thesis: verum