let h1, h2 be Function of the carrier' of C,(Maps (Hom C)); ( ( for f being Morphism of C holds h1 . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] ) & ( for f being Morphism of C holds h2 . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] ) implies h1 = h2 )
assume that
A9:
for f being Morphism of C holds h1 . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))]
and
A10:
for f being Morphism of C holds h2 . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))]
; h1 = h2
hence
h1 = h2
by FUNCT_2:63; verum