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

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

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;

hence o1 = o2 ; :: thesis: verum