theorem :: MSSUBFAM:20

for I being set
for A, B being ManySortedSet of I st A is non-empty & [|A,B|] is finite-yielding holds
B is finite-yielding