theorem Th7: :: FUNCT_7:7

for I being set
for M being ManySortedSet of I
for i being set st i in I holds
i .--> (M . i) = M | {i}