let x be object ; 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; 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; 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; ( <*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)
; (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; verum