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 A1, TREES_1:21;
A3: <*n*> ^ q in tree (doms p) by A1, Th10;
A4: len (doms p) = len p by TREES_3:38;
A5: q9 in (dom (x -tree p)) | <*n*> by A1, A2, TREES_1:def 6;
A6: n < len p by A3, A4, TREES_3:48;
A7: ( dom ((x -tree p) | <*n*>) = (dom (x -tree p)) | <*n*> & ((x -tree p) | <*n*>) . q9 = (x -tree p) . (<*n*> ^ q) ) by A5, TREES_2:def 10;
( n + 1 in dom p & p . (n + 1) = (x -tree p) | <*n*> ) by A6, Def4, Lm2;
hence (x -tree p) . (<*n*> ^ q) = p .. ((n + 1),q) by A5, A7, FUNCT_5:38; :: thesis: verum