:: deftheorem defines = PBOOLE:def 21 :
for I being non empty set
for A, B being ManySortedSet of I holds
( A = B iff for i being Element of I holds A . i = B . i );