:: deftheorem defines is_isomorphism ALG_1:def 4 :
for U1, U2 being Universal_Algebra
for f being Function of U1,U2 holds
( f is_isomorphism iff ( f is_monomorphism & f is_epimorphism ) );