let G, H 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 Th44, Th49;
then reconsider h9 = h " as Function of Imh,G by A1, FUNCT_2:25;

now :: thesis: for a, b being Element of Imh holds h9 . (a * b) = (h9 . a) * (h9 . b)

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:42;
a9 in Imh ;
then consider a1 being Element of G such that
A2: h . a1 = a9 by Th45;
b9 in Imh ;
then consider b1 being Element of G such that
A3: h . b1 = b9 by Th45;
thus h9 . (a * b) = h9 . ((h . a1) * (h . b1)) by A2, A3, GROUP_2:43
.= h9 . (h . (a1 * b1)) by Def6
.= a1 * b1 by A1, FUNCT_2:26
.= (h9 . a) * b1 by A1, A2, FUNCT_2:26
.= (h9 . a) * (h9 . b) by A1, A3, FUNCT_2:26 ; :: thesis: verum

end;

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