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