for I being set
for A being ManySortedSet of I
for B being V2() ManySortedSet of I
for F being ManySortedFunction of A,B st A is V2() holds
( F is "1-1" iff for C being ManySortedSet of I
for G, H being ManySortedFunction of C,A st F ** G = F ** H holds
G = H )