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)) ;

( 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 :: thesis: for f being Morphism of C holds ((curry T) . (id a)) . f = (hom?- a) . f

hence
hom?- a = (curry (hom?? C)) . (id a)
by FUNCT_2:63; :: thesis: hom-? a = (curry' (hom?? C)) . (id a)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 FUNCT_5:69

.= [[(Hom ((cod (id a)),(dom f))),(Hom ((dom (id a)),(cod f)))],(hom ((id a),f))] by Def23

.= [[(Hom ((cod (id a)),(dom f))),(Hom ((dom (id a)),(cod f)))],(hom (a,f))] by Th52

.= [[(Hom (a,(dom f))),(Hom ((dom (id a)),(cod f)))],(hom (a,f))]

.= [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))]

.= (hom?- a) . f by Def20 ; :: thesis: verum

end;thus ((curry T) . (id a)) . f = T . ((id a),f) by FUNCT_5:69

.= [[(Hom ((cod (id a)),(dom f))),(Hom ((dom (id a)),(cod f)))],(hom ((id a),f))] by Def23

.= [[(Hom ((cod (id a)),(dom f))),(Hom ((dom (id a)),(cod f)))],(hom (a,f))] by Th52

.= [[(Hom (a,(dom f))),(Hom ((dom (id a)),(cod f)))],(hom (a,f))]

.= [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))]

.= (hom?- a) . f by Def20 ; :: thesis: verum

now :: thesis: for f being Morphism of C holds ((curry' T) . (id a)) . f = (hom-? a) . f

hence
hom-? a = (curry' (hom?? C)) . (id a)
by FUNCT_2:63; :: thesis: verumlet 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 FUNCT_5:70

.= [[(Hom ((cod f),(dom (id a)))),(Hom ((dom f),(cod (id a))))],(hom (f,(id a)))] by Def23

.= [[(Hom ((cod f),(dom (id a)))),(Hom ((dom f),(cod (id a))))],(hom (f,a))] by Th52

.= [[(Hom ((cod f),a)),(Hom ((dom f),(cod (id a))))],(hom (f,a))]

.= [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))]

.= (hom-? a) . f by Def21 ; :: thesis: verum

end;thus ((curry' T) . (id a)) . f = T . (f,(id a)) by FUNCT_5:70

.= [[(Hom ((cod f),(dom (id a)))),(Hom ((dom f),(cod (id a))))],(hom (f,(id a)))] by Def23

.= [[(Hom ((cod f),(dom (id a)))),(Hom ((dom f),(cod (id a))))],(hom (f,a))] by Th52

.= [[(Hom ((cod f),a)),(Hom ((dom f),(cod (id a))))],(hom (f,a))]

.= [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))]

.= (hom-? a) . f by Def21 ; :: thesis: verum