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