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

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) ) )

hence
h1 = h2
by BINOP_1:2; :: thesis: verumthus
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;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