for I being set
for A, B being ManySortedSet of I st A c= B holds
for f being FinSequence of I holds A * f c= B * f