theorem Th45: :: YELLOW_7:45

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