for U1, U2 being Universal_Algebra
for h being Function of U1,U2 st h is_homomorphism holds
rng h = the carrier of (Image h)