theorem Th5: :: OSAFREE:5

for S being OrderSortedSign
for X being non-empty ManySortedSet of S
for o being OperSymbol of S
for x being set st x in (((ParsedTerms X) #) * the Arity of S) . o holds
x is FinSequence of TS (DTConOSA X)