theorem :: ENS_1:59

for V being non empty set
for C being Category
for a being Object of C
for f being Morphism of C st Hom C c= V holds
(hom?- (V,a)) . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))]