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