let C be Category; :: thesis: for a being Object of C holds
( hom?- a = (curry (hom?? C)) . (id a) & hom-? a = (curry' (hom?? C)) . (id a) )
let a be Object of C; :: thesis: ( hom?- a = (curry (hom?? C)) . (id a) & hom-? a = (curry' (hom?? C)) . (id a) )
reconsider T = hom?? C as Function of [:the carrier' of C,the carrier' of C:],(Maps (Hom C)) ;

now

let f be Morphism of C; :: thesis: ((curry T) . (id a)) . f = (hom?- a) . f
thus ((curry T) . (id a)) . f = T . (id a),f by CAT_2:3
.= [[(Hom (cod (id a)),(dom f)),(Hom (dom (id a)),(cod f))],(hom (id a),f)] by Def25
.= [[(Hom (cod (id a)),(dom f)),(Hom (dom (id a)),(cod f))],(hom a,f)] by Th53
.= [[(Hom a,(dom f)),(Hom (dom (id a)),(cod f))],(hom a,f)] by CAT_1:44
.= [[(Hom a,(dom f)),(Hom a,(cod f))],(hom a,f)] by CAT_1:44
.= (hom?- a) . f by Def22 ; :: thesis: verum

end;

hence hom?- a = (curry (hom?? C)) . (id a) by FUNCT_2:113; :: thesis: hom-? a = (curry' (hom?? C)) . (id a)

now

let f be Morphism of C; :: thesis: ((curry' T) . (id a)) . f = (hom-? a) . f
thus ((curry' T) . (id a)) . f = T . f,(id a) by CAT_2:4
.= [[(Hom (cod f),(dom (id a))),(Hom (dom f),(cod (id a)))],(hom f,(id a))] by Def25
.= [[(Hom (cod f),(dom (id a))),(Hom (dom f),(cod (id a)))],(hom f,a)] by Th53
.= [[(Hom (cod f),a),(Hom (dom f),(cod (id a)))],(hom f,a)] by CAT_1:44
.= [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)] by CAT_1:44
.= (hom-? a) . f by Def23 ; :: thesis: verum

end;

hence hom-? a = (curry' (hom?? C)) . (id a) by FUNCT_2:113; :: thesis: verum