theorem Th4: :: PBOOLE:4

for I being set
for X, Y being ManySortedSet of I
for i being object st i in I holds
(X (\+\) Y) . i = (X . i) \+\ (Y . i)