for I being set
for A being V2() V35() ManySortedSet of I ex F being ManySortedFunction of I --> NAT,A st F is "onto"