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,a))) . b = Hom (b,a)

let C be Category; :: thesis: for a, b being Object of C st Hom C c= V holds

(Obj (hom-? (V,a))) . b = Hom (b,a)

let a, b be Object of C; :: thesis: ( Hom C c= V implies (Obj (hom-? (V,a))) . b = Hom (b,a) )

assume A1: Hom C c= V ; :: thesis: (Obj (hom-? (V,a))) . b = Hom (b,a)

Hom (b,a) in Hom C ;

then reconsider A = Hom (b,a) as Element of V by A1;

set d = @ A;

(hom-? (V,a)) . (id b) = (hom-? a) . (id b) by A1, Def25

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

hence (Obj (hom-? (V,a))) . b = Hom (b,a) by OPPCAT_1:30; :: thesis: verum

for a, b being Object of C st Hom C c= V holds

(Obj (hom-? (V,a))) . b = Hom (b,a)

let C be Category; :: thesis: for a, b being Object of C st Hom C c= V holds

(Obj (hom-? (V,a))) . b = Hom (b,a)

let a, b be Object of C; :: thesis: ( Hom C c= V implies (Obj (hom-? (V,a))) . b = Hom (b,a) )

assume A1: Hom C c= V ; :: thesis: (Obj (hom-? (V,a))) . b = Hom (b,a)

Hom (b,a) in Hom C ;

then reconsider A = Hom (b,a) as Element of V by A1;

set d = @ A;

(hom-? (V,a)) . (id b) = (hom-? a) . (id b) by A1, Def25

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

hence (Obj (hom-? (V,a))) . b = Hom (b,a) by OPPCAT_1:30; :: thesis: verum