let o1, o2 be BinComp of (the_hom_sets_of C); :: thesis: ( ( for i, j, k being Object of C holds o1 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] ) & ( for i, j, k being Object of C holds o2 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] ) implies o1 = o2 )

assume that

A15: for i, j, k being Object of C holds o1 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] and

A16: for i, j, k being Object of C holds o2 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] ; :: thesis: o1 = o2

assume that

A15: for i, j, k being Object of C holds o1 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] and

A16: for i, j, k being Object of C holds o2 . (i,j,k) = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] ; :: thesis: o1 = o2

now :: thesis: for a being object st a in [: the carrier of C, the carrier of C, the carrier of C:] holds

o1 . a = o2 . a

hence
o1 = o2
; :: thesis: verumo1 . a = o2 . a

let a be object ; :: thesis: ( a in [: the carrier of C, the carrier of C, the carrier of C:] implies o1 . a = o2 . a )

assume a in [: the carrier of C, the carrier of C, the carrier of C:] ; :: thesis: o1 . a = o2 . a

then consider i, j, k being Object of C such that

A17: a = [i,j,k] by DOMAIN_1:3;

thus o1 . a = o1 . (i,j,k) by A17, MULTOP_1:def 1

.= the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] by A15

.= o2 . (i,j,k) by A16

.= o2 . a by A17, MULTOP_1:def 1 ; :: thesis: verum

end;assume a in [: the carrier of C, the carrier of C, the carrier of C:] ; :: thesis: o1 . a = o2 . a

then consider i, j, k being Object of C such that

A17: a = [i,j,k] by DOMAIN_1:3;

thus o1 . a = o1 . (i,j,k) by A17, MULTOP_1:def 1

.= the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] by A15

.= o2 . (i,j,k) by A16

.= o2 . a by A17, MULTOP_1:def 1 ; :: thesis: verum