:: deftheorem Def23 defines hom?? ENS_1:def 24 :
for C being Category
for b₂ being Function of the carrier' of [:C,C:],(Maps (Hom C)) holds
( b₂ = hom?? C iff for f, g being Morphism of C holds b₂ . [f,g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] );