for U1 being Universal_Algebra
for U2 being strict Universal_Algebra
for f being Function of U1,U2 st f is_homomorphism holds
( f is_epimorphism iff Image f = U2 )