theorem :: TREES_4:19

for x being object
for p being DTree-yielding FinSequence
for n being Nat
for q being FinSequence st <*n*> ^ q in dom (x -tree p) holds
(x -tree p) . (<*n*> ^ q) = p .. ((n + 1),q)