let H, G 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 Th53, FUNCT_2:def 1;
then reconsider f9 = h as Function of G,(Image h) by RELSET_1:4;

now

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 Def7 ; :: thesis: verum

end;

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