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:3;
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