theorem Th1: :: CLOSURE3:1

for I being non empty set
for M, N being ManySortedSet of I holds M +* N = N