:: deftheorem Def2 defines ArgumentSeq MSATERM:def 2 :
for S being non empty non void ManySortedSign
for V being non-empty ManySortedSet of the carrier of S
for sy being NonTerminal of (DTConMSA V)
for b₄ being FinSequence of S -Terms V holds
( b₄ is ArgumentSeq of sy iff b₄ is SubtreeSeq of sy );