for I being set
for A, B being ManySortedSet of I
for M being ManySortedSubset of A
for F being ManySortedFunction of A,B holds F .:.: M c= F .:.: A