let U1 be Universal_Algebra; :: thesis: for E being Congruence of U1 holds Nat_Hom U1,E is_epimorphism U1, QuotUnivAlg U1,E
let E be Congruence of U1; :: thesis: Nat_Hom U1,E is_epimorphism U1, QuotUnivAlg U1,E
set f = Nat_Hom U1,E;
set qa = QuotUnivAlg U1,E;
set cqa = the carrier of (QuotUnivAlg U1,E);
set u1 = the carrier of U1;
thus Nat_Hom U1,E is_homomorphism U1, QuotUnivAlg U1,E by Th21; :: according to ALG_1:def 3 :: thesis: rng (Nat_Hom U1,E) = the carrier of (QuotUnivAlg U1,E)
thus rng (Nat_Hom U1,E) c= the carrier of (QuotUnivAlg U1,E) ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of (QuotUnivAlg U1,E) c= rng (Nat_Hom U1,E)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (QuotUnivAlg U1,E) or x in rng (Nat_Hom U1,E) )
assume A1: x in the carrier of (QuotUnivAlg U1,E) ; :: thesis: x in rng (Nat_Hom U1,E)
then reconsider x1 = x as Subset of the carrier of U1 ;
consider y being set such that
A2: y in the carrier of U1 and
A3: x1 = Class E,y by A1, EQREL_1:def 5;
reconsider y = y as Element of the carrier of U1 by A2;
dom (Nat_Hom U1,E) = the carrier of U1 by FUNCT_2:def 1;
then (Nat_Hom U1,E) . y in rng (Nat_Hom U1,E) by FUNCT_1:def 5;
hence x in rng (Nat_Hom U1,E) by A3, Def15; :: thesis: verum