for J being set
for D being non empty set
for K being ManySortedSet of J
for F being DoubleIndexedSet of K,D holds doms F = K