let x be object ; :: thesis: 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)

let p be DTree-yielding FinSequence; :: thesis: 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)

let n be Nat; :: thesis: for q being FinSequence st <*n*> ^ q in dom (x -tree p) holds
(x -tree p) . (<*n*> ^ q) = p .. ((n + 1),q)

let q be FinSequence; :: thesis: ( <*n*> ^ q in dom (x -tree p) implies (x -tree p) . (<*n*> ^ q) = p .. ((n + 1),q) )
assume A1: <*n*> ^ q in dom (x -tree p) ; :: thesis: (x -tree p) . (<*n*> ^ q) = p .. ((n + 1),q)
then <*n*> ^ q is Node of (x -tree p) ;
then reconsider q9 = q as FinSequence of NAT by FINSEQ_1:36;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A2: <*n*> in dom (x -tree p) by ;
A3: <*n*> ^ q in tree (doms p) by ;
A4: len (doms p) = len p by TREES_3:38;
A5: q9 in (dom (x -tree p)) | <*n*> by ;
A6: n < len p by ;
A7: ( dom ((x -tree p) | <*n*>) = (dom (x -tree p)) | <*n*> & ((x -tree p) | <*n*>) . q9 = (x -tree p) . (<*n*> ^ q) ) by ;
( n + 1 in dom p & p . (n + 1) = (x -tree p) | <*n*> ) by ;
hence (x -tree p) . (<*n*> ^ q) = p .. ((n + 1),q) by ; :: thesis: verum