let V be non empty set ; :: thesis: 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)]
let C be Category; :: thesis: 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)]
let f, g be Morphism of C; :: thesis: ( Hom C c= V implies (hom?? V,C) . [(f opp ),g] = [[(Hom (cod f),(dom g)),(Hom (dom f),(cod g))],(hom f,g)] )
assume A1: Hom C c= V ; :: thesis: (hom?? V,C) . [(f opp ),g] = [[(Hom (cod f),(dom g)),(Hom (dom f),(cod g))],(hom f,g)]
thus (hom?? V,C) . [(f opp ),g] = (hom?? V,C) . [f,g] by OPPCAT_1:def 4
.= (hom?? C) . [f,g] by A1, Def28
.= [[(Hom (cod f),(dom g)),(Hom (dom f),(cod g))],(hom f,g)] by Def25 ; :: thesis: verum