theorem :: ENS_1:63

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