theorem :: ENS_1:65
for V being non empty set
for C being Category
for a being Object of C st Hom C c= V holds
(hom?? (V,C)) ?- (a opp) = hom?- (V,a)