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 q' = q as FinSequence of NAT by FINSEQ_1:50;
( <*n*> in dom (x -tree p) & <*n*> ^ q in tree (doms p) & len (doms p) = len p ) by A1, Th10, TREES_1:46, TREES_3:40;
then A2: ( q' in (dom (x -tree p)) | <*n*> & n < len p ) by A1, TREES_1:def 9, TREES_3:51;
then ( dom ((x -tree p) | <*n*>) = (dom (x -tree p)) | <*n*> & n + 1 in dom p & ((x -tree p) | <*n*>) . q' = (x -tree p) . (<*n*> ^ q) & p . (n + 1) = (x -tree p) | <*n*> ) by Def4, Lm2, TREES_2:def 11;
hence (x -tree p) . (<*n*> ^ q) = p .. (n + 1),q by A2, FUNCT_5:45; :: thesis: verum