theorem Th36: :: TREES_9:36

for T being finite-branching DecoratedTree
for t being Element of dom T holds succ (T,t) = T * (t succ)