for I being set
for f being Function
for M being ManySortedSet of I holds (f +* M) | I = M