theorem Th4: :: MSUHOM_1:4

for I being set
for C being Subset of I
for M being ManySortedSet of I holds (M | C) # = (M #) | (C *)