let U1 be Universal_Algebra; for E being Congruence of U1 holds Nat_Hom (U1,E) is_epimorphism
let E be Congruence of U1; 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; ALG_1:def 3 rng (Nat_Hom (U1,E)) = the carrier of (QuotUnivAlg (U1,E))
thus
rng (Nat_Hom (U1,E)) c= the carrier of (QuotUnivAlg (U1,E))
; XBOOLE_0:def 10 the carrier of (QuotUnivAlg (U1,E)) c= rng (Nat_Hom (U1,E))
let x be object ; TARSKI:def 3 ( 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))
; 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; verum