theorem Th13: :: OSAFREE:13

for S being OrderSortedSign
for X being non-empty ManySortedSet of S
for o being OperSymbol of S
for x being FinSequence holds
( x in Args (o,(ParsedTermsOSA X)) iff ( x is FinSequence of TS (DTConOSA X) & OSSym (o,X) ==> roots x ) )