let U1, U2 be Universal_Algebra; :: thesis: for h being Function of U1,U2 st h is_homomorphism holds
rng h = the carrier of (Image h)
let h be Function of U1,U2; :: thesis: ( h is_homomorphism implies rng h = the carrier of (Image h) )
dom h = the carrier of U1 by FUNCT_2:def 1;
then A1: rng h = h .: the carrier of U1 by RELAT_1:113;
assume h is_homomorphism ; :: thesis: rng h = the carrier of (Image h)
hence rng h = the carrier of (Image h) by A1, Def6; :: thesis: verum