for U1, U2 being Universal_Algebra
for f being Function of U1,U2 st f is_epimorphism holds
QuotUnivAlg (U1,(Cng f)),U2 are_isomorphic