let G, H be Group; :: thesis: for h being Homomorphism of G,H holds h is Homomorphism of G,(Image h)
let h be Homomorphism of G,H; :: thesis: h is Homomorphism of G,(Image h)
( rng h = the carrier of (Image h) & dom h = the carrier of G ) by Th44, FUNCT_2:def 1;
then reconsider f9 = h as Function of G,(Image h) by RELSET_1:4;

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

let a, b be Element of G; :: thesis: (f9 . a) * (f9 . b) = f9 . (a * b)
thus (f9 . a) * (f9 . b) = (h . a) * (h . b) by GROUP_2:43
.= f9 . (a * b) by Def6 ; :: thesis: verum

end;

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