theorem :: MSAFREE:2

for I being set
for X being ManySortedSet of I
for i being set st i in I holds
( X . i <> {} iff (coprod X) . i <> {} )