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 )
assume A1: h is one-to-one ; :: thesis: G, Image h are_isomorphic
reconsider ih = h as Homomorphism of G,(Image h) by Th58;
take ih ; :: according to GROUP_6:def 15 :: thesis: ih is bijective
A2: ih is one-to-one by A1;

now

the carrier of (Image h) = rng ih by Th53;
hence ih is onto by FUNCT_2:def 3; :: thesis: verum

end;

hence ih is bijective by A2; :: thesis: verum