let U1, U2 be Universal_Algebra; :: thesis: for f being Function of U1,U2 st f is_epimorphism U1,U2 holds
HomQuot f is_isomorphism QuotUnivAlg U1,(Cng f),U2
let f be Function of U1,U2; :: thesis: ( f is_epimorphism U1,U2 implies HomQuot f is_isomorphism QuotUnivAlg U1,(Cng f),U2 )
set qa = QuotUnivAlg U1,(Cng f);
set u1 = the carrier of U1;
set u2 = the carrier of U2;
set F = HomQuot f;
assume A1: f is_epimorphism U1,U2 ; :: thesis: HomQuot f is_isomorphism QuotUnivAlg U1,(Cng f),U2
then A2: f is_homomorphism U1,U2 by Def3;
then HomQuot f is_monomorphism QuotUnivAlg U1,(Cng f),U2 by Th23;
then A3: HomQuot f is one-to-one by Def2;
A4: rng f = the carrier of U2 by A1, Def3;
A5: rng (HomQuot f) = the carrier of U2

proof

thus rng (HomQuot f) c= the carrier of U2 ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of U2 c= rng (HomQuot f)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of U2 or x in rng (HomQuot f) )
assume x in the carrier of U2 ; :: thesis: x in rng (HomQuot f)
then consider y being set such that
A6: y in dom f and
A7: f . y = x by A4, FUNCT_1:def 5;
reconsider y = y as Element of the carrier of U1 by A6;
set u = Class (Cng f),y;
A8: ( dom (HomQuot f) = the carrier of (QuotUnivAlg U1,(Cng f)) & Class (Cng f),y in Class (Cng f) ) by EQREL_1:def 5, FUNCT_2:def 1;
(HomQuot f) . (Class (Cng f),y) = x by A2, A7, Def17;
hence x in rng (HomQuot f) by A8, FUNCT_1:def 5; :: thesis: verum

end;

HomQuot f is_homomorphism QuotUnivAlg U1,(Cng f),U2 by A2, Th23;
hence HomQuot f is_isomorphism QuotUnivAlg U1,(Cng f),U2 by A3, A5, Th8; :: thesis: verum