:: deftheorem Def11 defines Nat_Hom ALG_1:def 11 :
for U1 being Universal_Algebra
for E being Congruence of U1
for b₃ being Function of U1,(QuotUnivAlg (U1,E)) holds
( b₃ = Nat_Hom (U1,E) iff for u being Element of U1 holds b₃ . u = Class (E,u) );