let U1, U2 be Universal_Algebra; for f being Function of U1,U2 st f is_epimorphism holds
QuotUnivAlg (U1,(Cng f)),U2 are_isomorphic
let f be Function of U1,U2; ( f is_epimorphism implies QuotUnivAlg (U1,(Cng f)),U2 are_isomorphic )
assume A1:
f is_epimorphism
; QuotUnivAlg (U1,(Cng f)),U2 are_isomorphic
take
HomQuot f
; ALG_1:def 5 HomQuot f is_isomorphism
thus
HomQuot f is_isomorphism
by A1, Th20; verum