theorem :: ENS_1:64

for V being non empty set
for C being Category
for a, b being Object of C st Hom C c= V holds
(Obj (hom?? (V,C))) . [(a opp),b] = Hom (a,b)