:: deftheorem Def18 defines hom ENS_1:def 19 :
for C being Category
for a being Object of C
for f being Morphism of C
for b₄ being Function of (Hom (a,(dom f))),(Hom (a,(cod f))) holds
( b₄ = hom (a,f) iff for g being Morphism of C st g in Hom (a,(dom f)) holds
b₄ . g = f (*) g );