let U1, U2 be Universal_Algebra; :: thesis: for f being Function of U1,U2 st f is_epimorphism holds
HomQuot f is_isomorphism
let f be Function of U1,U2; :: thesis: ( f is_epimorphism implies HomQuot f is_isomorphism )
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 ; :: thesis: HomQuot f is_isomorphism
then A2: f is_homomorphism ;
then HomQuot f is_monomorphism by Th19;
then A3: HomQuot f is one-to-one ;
A4: rng f = the carrier of U2 by A1;
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 object ; :: 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 object 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, Def13;
hence x in rng (HomQuot f) by A8, FUNCT_1:def 3; :: thesis: verum

end;

HomQuot f is_homomorphism by A2, Th19;
hence HomQuot f is_isomorphism by A3, A5, Th7; :: thesis: verum