theorem Th12: :: TREES_4:12

for x being object
for p being DTree-yielding FinSequence
for i being Nat
for T being DecoratedTree
for q being Node of T st i < len p & T = p . (i + 1) holds
(x -tree p) . (<*i*> ^ q) = T . q