let U1, U2 be Universal_Algebra; :: thesis: 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; :: thesis: ( f is_epimorphism implies QuotUnivAlg (U1,(Cng f)),U2 are_isomorphic )
assume A1: f is_epimorphism ; :: thesis: QuotUnivAlg (U1,(Cng f)),U2 are_isomorphic
take HomQuot f ; :: according to ALG_1:def 5 :: thesis: HomQuot f is_isomorphism
thus HomQuot f is_isomorphism by A1, Th20; :: thesis: verum