let H, G be Group; :: thesis: for h being Homomorphism of G,H st h is one-to-one holds
h " is Homomorphism of (Image h),G
let h be Homomorphism of G,H; :: thesis: ( h is one-to-one implies h " is Homomorphism of (Image h),G )
assume A1: h is one-to-one ; :: thesis: h " is Homomorphism of (Image h),G
reconsider Imh = Image h as Group ;
( h is Function of G,Imh & rng h = the carrier of Imh ) by Th53, Th58;
then reconsider h9 = h " as Function of Imh,G by A1, FUNCT_2:31;

now

let a, b be Element of Imh; :: thesis: h9 . (a * b) = (h9 . a) * (h9 . b)
reconsider a9 = a, b9 = b as Element of H by GROUP_2:51;
a9 in Imh by STRUCT_0:def 5;
then consider a1 being Element of G such that
A2: h . a1 = a9 by Th54;
b9 in Imh by STRUCT_0:def 5;
then consider b1 being Element of G such that
A3: h . b1 = b9 by Th54;
thus h9 . (a * b) = h9 . ((h . a1) * (h . b1)) by A2, A3, GROUP_2:52
.= h9 . (h . (a1 * b1)) by Def7
.= a1 * b1 by A1, FUNCT_2:32
.= (h9 . a) * b1 by A1, A2, FUNCT_2:32
.= (h9 . a) * (h9 . b) by A1, A3, FUNCT_2:32 ; :: thesis: verum

end;

hence h " is Homomorphism of (Image h),G by Def7; :: thesis: verum