for I being set
for Y being non empty set
for x being b₂ -valued ManySortedSet of I
for p being FinSequence of I holds p * x is FinSequence of Y