theorem Th17: :: OSAFREE:17

for S being OrderSortedSign
for X being non-empty ManySortedSet of S
for o being OperSymbol of S
for x being Element of Args (o,(ParsedTermsOSA X))
for t being Element of TS (DTConOSA X) st t = (Den (o,(ParsedTermsOSA X))) . x holds
LeastSort t = the_result_sort_of o