for S being OrderSortedSign
for X being V2() 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 ) )