theorem :: MSSUBFAM:24

for I being set
for F being ManySortedFunction of I st doms F is finite-yielding holds
rngs F is finite-yielding