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 3;
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 3, 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 3; :: 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