theorem Th9: :: MSUALG_9:9

for I being set
for A being non-empty ManySortedSet of I
for B being ManySortedSet of I
for F being ManySortedFunction of A,{B} holds F is "onto"