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