theorem Th40: :: TREES_9:40

for T being finite-branching DecoratedTree
for x being FinSequence
for n being Nat st x ^ <*n*> in dom T holds
T . (x ^ <*n*>) = (succ (T,x)) . (n + 1)