:: deftheorem Def13 defines HomQuot ALG_1:def 13 :
for U1, U2 being Universal_Algebra
for f being Function of U1,U2 st f is_homomorphism holds
for b₄ being Function of (QuotUnivAlg (U1,(Cng f))),U2 holds
( b₄ = HomQuot f iff for a being Element of U1 holds b₄ . (Class ((Cng f),a)) = f . a );