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
then A2: h is one-to-one ;
reconsider Imh = Image h as Group ;
h " is Function of Imh,G

proof

A3: h is Function of G,Imh by Th58;
rng h = the carrier of Imh by Th53;
hence h " is Function of Imh,G by A1, A3, FUNCT_2:31; :: thesis: verum

end;

then reconsider h' = h " as Function of Imh,G ;

now

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

end;

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