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;

A2: id (a opp) = id a by OPPCAT_1:71;

set d = @ A;

(hom?? (V,C)) . (id [(a opp),b]) = (hom?? (V,C)) . [(id (a opp)),(id b)] by CAT_2:31

.= (hom?? C) . [(id a),(id b)] by A1, Def26, A2

.= id (@ A) by A1, Lm11 ;

hence (Obj (hom?? (V,C))) . [(a opp),b] = Hom (a,b) by CAT_1:67; :: thesis: verum

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;

A2: id (a opp) = id a by OPPCAT_1:71;

set d = @ A;

(hom?? (V,C)) . (id [(a opp),b]) = (hom?? (V,C)) . [(id (a opp)),(id b)] by CAT_2:31

.= (hom?? C) . [(id a),(id b)] by A1, Def26, A2

.= id (@ A) by A1, Lm11 ;

hence (Obj (hom?? (V,C))) . [(a opp),b] = Hom (a,b) by CAT_1:67; :: thesis: verum