theorem :: MSUALG_9:12

for I being set
for A being non-empty finite-yielding ManySortedSet of I ex F being ManySortedFunction of I --> NAT,A st F is "onto"