let V be non empty set ; :: thesis: for C being Category
for a, b being Object of C st Hom C c= V holds
(Obj (hom?? V,C)) . [(a opp ),b] = Hom a,b
let C be Category; :: thesis: for a, b being Object of C st Hom C c= V holds
(Obj (hom?? V,C)) . [(a opp ),b] = Hom a,b
let a, b be Object of C; :: thesis: ( Hom C c= V implies (Obj (hom?? V,C)) . [(a opp ),b] = Hom a,b )
assume A1: Hom C c= V ; :: thesis: (Obj (hom?? V,C)) . [(a opp ),b] = Hom a,b
Hom a,b in Hom C ;
then reconsider A = Hom a,b as Element of V by A1;
set d = @ A;
(hom?? V,C) . (id [(a opp ),b]) = (hom?? V,C) . [(id (a opp )),(id b)] by CAT_2:41
.= (hom?? V,C) . [((id a) opp ),(id b)] by OPPCAT_1:21
.= (hom?? V,C) . [(id a),(id b)] by OPPCAT_1:def 4
.= (hom?? C) . [(id a),(id b)] by A1, Def28
.= id (@ A) by A1, Lm10 ;
hence (Obj (hom?? V,C)) . [(a opp ),b] = Hom a,b by CAT_1:103; :: thesis: verum