let U1 be Universal_Algebra; :: thesis: for E being Congruence of U1 holds Nat_Hom (U1,E) is_epimorphism
let E be Congruence of U1; :: thesis: Nat_Hom (U1,E) is_epimorphism
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 by Th17; :: 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 object ; :: 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 object such that
A2: y in the carrier of U1 and
A3: x1 = Class (E,y) by A1, EQREL_1:def 3;
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 3;
hence x in rng (Nat_Hom (U1,E)) by A3, Def11; :: thesis: verum