for f being Function
for I being set
for A, B being ManySortedSet of I st ( for i being set st i in I holds
( A . i c= dom f & f .: (A . i) c= B . i ) ) holds
f -MSF (I,A) is ManySortedFunction of A,B