theorem Th7: :: OSAFREE:7

for S being OrderSortedSign
for X being non-empty ManySortedSet of S
for o being OperSymbol of S
for p being FinSequence of TS (DTConOSA X) holds
( OSSym (o,X) ==> roots p iff p in (((ParsedTerms X) #) * the Arity of S) . o )