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 :: thesis: for f being Morphism of C holds ((curry T) . (id a)) . f = (hom?- a) . f
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;
hence hom?- a = (curry (hom?? C)) . (id a) by FUNCT_2:63; :: thesis: hom-? a = (curry' (hom?? C)) . (id a)
now :: thesis: for f being Morphism of C holds ((curry' T) . (id a)) . f = (hom-? a) . f
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 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;
hence hom-? a = (curry' (hom?? C)) . (id a) by FUNCT_2:63; :: thesis: verum