theorem Th8: :: OSAFREE:8

for S being OrderSortedSign
for X being non-empty ManySortedSet of S holds union (rng (ParsedTerms X)) = TS (DTConOSA X)