:: deftheorem Def21 defines hom-? ENS_1:def 22 :
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 ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] );