theorem Th8: :: TREES_9:8

for t being finite-branching DecoratedTree ex x being set ex p being DTree-yielding FinSequence st t = x -tree p