for I being set
for A, B, C being V5() ManySortedSet of I
for f being ManySortedFunction of A,B st B is ManySortedSubset of C holds
f is ManySortedFunction of A,C