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

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