let h1, h2 be Function of the carrier' of [:C,C:],(Maps (Hom C)); :: thesis: ( ( for f, g being Morphism of C holds h1 . [f,g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] ) & ( for f, g being Morphism of C holds h2 . [f,g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] ) implies h1 = h2 )
assume that
A5: for f, g being Morphism of C holds h1 . [f,g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] and
A6: for f, g being Morphism of C holds h2 . [f,g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] ; :: thesis: h1 = h2

now :: thesis: ( the carrier' of [:C,C:] = [: the carrier' of C, the carrier' of C:] & ( for f, g being Morphism of C holds h1 . (f,g) = h2 . (f,g) ) )

thus the carrier' of [:C,C:] = [: the carrier' of C, the carrier' of C:] ; :: thesis: for f, g being Morphism of C holds h1 . (f,g) = h2 . (f,g)
let f, g be Morphism of C; :: thesis: h1 . (f,g) = h2 . (f,g)
thus h1 . (f,g) = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] by A5
.= h2 . (f,g) by A6 ; :: thesis: verum

end;

hence h1 = h2 by BINOP_1:2; :: thesis: verum