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 = hom-? (V,a)

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

(hom?? (V,C)) -? a = hom-? (V,a)

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

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

hence (hom?? (V,C)) -? a = (curry' (hom?? C)) . (id a) by Def26

.= hom-? a by Th56

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

:: thesis: verum

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

(hom?? (V,C)) -? a = hom-? (V,a)

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

(hom?? (V,C)) -? a = hom-? (V,a)

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

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

hence (hom?? (V,C)) -? a = (curry' (hom?? C)) . (id a) by Def26

.= hom-? a by Th56

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

:: thesis: verum