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
A16: 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
A17: 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

let a be set ; :: 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
A18: a = [i,j,k] by DOMAIN_1:15;
thus o1 . a = o1 . i,j,k by A18, MULTOP_1:def 1
.= the Comp of C | [:((the_hom_sets_of C) . j,k),((the_hom_sets_of C) . i,j):] by A16
.= o2 . i,j,k by A17
.= o2 . a by A18, MULTOP_1:def 1 ; :: thesis: verum

end;

hence o1 = o2 by PBOOLE:3; :: thesis: verum