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