for I being set
for Y, Z being ManySortedSet of I st ( for i, j being object st i in I & j in I & i <> j holds
(Y . i) /\ (Z . j) = {} ) holds
Union (Y (\) Z) = (Union Y) \ (Union Z)