for t being finite DecoratedTree
for x being set
for p being DTree-yielding FinSequence st t = x -tree p holds
for n being empty Element of dom t holds succ (t,n) = roots p