theorem :: TREES_3:48

for n being Nat
for p, q being FinSequence st p is Tree-yielding holds
( <*n*> ^ q in tree p iff ( n < len p & q in p . (n + 1) ) )