theorem Th1: :: HILBERT2:1

for Z being set
for M being ManySortedSet of Z st ( for x being set st x in Z holds
M . x is ManySortedSet of x ) holds
for f being Function st f = Union M holds
dom f = union Z