:: deftheorem Def4 defines -tree TREES_4:def 4 :
for x being object
for p being FinSequence st p is DTree-yielding holds
for b₃ being DecoratedTree holds
( b₃ = x -tree p iff ( ex q being DTree-yielding FinSequence st
( p = q & dom b₃ = tree (doms q) ) & b₃ . {} = x & ( for n being Nat st n < len p holds
b₃ | <*n*> = p . (n + 1) ) ) );