for I being set
for A being ManySortedSet of I
for F being ManySortedFunction of I st A c= rngs F holds
F .:.: (F "" A) = A