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