theorem Th1: :: INT_7:1

for x being object
for X being set
for p being ManySortedSet of X st support p = {x} holds
p = (X --> 0) +* (x,(p . x))