let o1, o2 be BinComp of (); :: thesis: ( ( for i, j, k being Object of C holds o1 . (i,j,k) = the Comp of C | [:(() . (j,k)),(() . (i,j)):] ) & ( for i, j, k being Object of C holds o2 . (i,j,k) = the Comp of C | [:(() . (j,k)),(() . (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 | [:(() . (j,k)),(() . (i,j)):] and
A16: for i, j, k being Object of C holds o2 . (i,j,k) = the Comp of C | [:(() . (j,k)),(() . (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
.= the Comp of C | [:(() . (j,k)),(() . (i,j)):] by A15
.= o2 . (i,j,k) by A16
.= o2 . a by ; :: thesis: verum
end;
hence o1 = o2 ; :: thesis: verum