for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B holds
( F is "onto" iff rngs F = B )