theorem Th39: :: TREES_9:39

for T being finite-branching DecoratedTree
for t being Element of dom T
for n being Nat holds
( t ^ <*n*> in dom T iff n + 1 in dom (t succ) )