:: deftheorem defines is_epimorphism ALG_1:def 3 :
for U1, U2 being Universal_Algebra
for f being Function of U1,U2 holds
( f is_epimorphism iff ( f is_homomorphism & rng f = the carrier of U2 ) );