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)
A2: id (a opp) = id a by OPPCAT_1:71;
thus (hom?? (V,C)) ?- (a opp) = (curry (hom?? C)) . (id a) by A1, Def26, A2
.= hom?- a by Th56
.= hom?- (V,a) by A1, Def24 ; :: thesis: verum