theorem Th8: :: OSAFREE:8

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