let x be set ; :: thesis: for p being DTree-yielding FinSequence
for n being Element of 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 Element of 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 Element of 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:50;
A3: <*n*> in dom (x -tree p) by A1, TREES_1:46;
A4: <*n*> ^ q in tree (doms p) by A1, Th10;
A5: len (doms p) = len p by TREES_3:40;
A6: q9 in (dom (x -tree p)) | <*n*> by A1, A3, TREES_1:def 9;
A7: n < len p by A4, A5, TREES_3:51;
A8: ( dom ((x -tree p) | <*n*>) = (dom (x -tree p)) | <*n*> & ((x -tree p) | <*n*>) . q9 = (x -tree p) . (<*n*> ^ q) ) by A6, TREES_2:def 11;
( n + 1 in dom p & p . (n + 1) = (x -tree p) | <*n*> ) by A7, Def4, Lm2;
hence (x -tree p) . (<*n*> ^ q) = p .. ((n + 1),q) by A6, A8, FUNCT_5:45; :: thesis: verum