theorem Th7: :: ABCMIZ_1:7

for S being non void Signature
for X being empty-yielding ManySortedSet of the carrier of S
for t being Element of (Free (S,X)) holds
( ex s being SortSymbol of S ex v being set st
( t = root-tree [v,s] & v in X . s ) or ex o being OperSymbol of S ex p being FinSequence of (Free (S,X)) st
( t = [o, the carrier of S] -tree p & len p = len (the_arity_of o) & p is DTree-yielding & p is ArgumentSeq of Sym (o,(X (\/) ( the carrier of S --> {0}))) ) )