for I being set
for A being ManySortedSet of I
for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds
Mpr1 F is "onto"