:: deftheorem Def20 defines hom?- ENS_1:def 21 :
for C being Category
for a being Object of C
for b₃ being Function of the carrier' of C,(Maps (Hom C)) holds
( b₃ = hom?- a iff for f being Morphism of C holds b₃ . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] );