for I being set
for A, B being V2() ManySortedSet of I
for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds
( F "" is "1-1" & F "" is "onto" )