let V be non empty set ; :: thesis: for C being Category
for a being Object of C st Hom C c= V holds
(hom?? V,C) ?- (a opp ) = hom?- V,a
let C be Category; :: thesis: for a being Object of C st Hom C c= V holds
(hom?? V,C) ?- (a opp ) = hom?- V,a
let a be Object of C; :: thesis: ( Hom C c= V implies (hom?? V,C) ?- (a opp ) = hom?- V,a )
assume A1: Hom C c= V ; :: thesis: (hom?? V,C) ?- (a opp ) = hom?- V,a
thus (hom?? V,C) ?- (a opp ) = (curry (hom?? V,C)) . ((id a) opp ) by OPPCAT_1:21
.= (curry (hom?? V,C)) . (id a) by OPPCAT_1:def 4
.= (curry (hom?? C)) . (id a) by A1, Def28
.= hom?- a by Th57
.= hom?- V,a by A1, Def26 ; :: thesis: verum