theorem Th38: :: TREES_9:38

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