theorem Th1: :: MSATERM:1

for S being non empty non void ManySortedSign
for V being non-empty ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being FinSequence holds
( ( [o, the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) iff a is ArgumentSeq of Sym (o,V) )