theorem Th1: :: PZFMISC1:1

for i being object
for I being set
for X being object
for M being ManySortedSet of I st i in I holds
dom (M +* (i .--> X)) = I