theorem :: PBOOLE:143
for I, Y being non empty set
for M being b2 -valued ManySortedSet of I
for x being Element of I holds M . x = M /. x