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)
h is Function of G,(Image h)

proof

A1: rng h = the carrier of (Image h) by Th53;
dom h = the carrier of G by FUNCT_2:def 1;
hence h is Function of G,(Image h) by A1, RELSET_1:11; :: thesis: verum

end;

then reconsider f' = h as Function of G,(Image h) ;

now

let a, b be Element of G; :: thesis: (f' . a) * (f' . b) = f' . (a * b)
thus (f' . a) * (f' . b) = (h . a) * (h . b) by GROUP_2:52
.= f' . (a * b) by Def7 ; :: thesis: verum

end;

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