for I being set
for Y being non empty set
for p being b₁ -defined b₂ -valued Function ex s being b₂ -valued ManySortedSet of I st p c= s