let h1, h2 be Function of the carrier' of C,(Maps (Hom C)); :: thesis: ( ( 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)] ; :: thesis: h1 = h2

now

let f be Morphism of C; :: thesis: h1 . f = h2 . f
thus h1 . f = [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)] by A9
.= h2 . f by A10 ; :: thesis: verum

end;

hence h1 = h2 by FUNCT_2:113; :: thesis: verum