let x be set ; :: thesis: for p being DTree-yielding FinSequence
for i being Element of NAT
for T being DecoratedTree
for q being Node of T st i < len p & T = p . (i + 1) holds
(x -tree p) . (<*i*> ^ q) = T . q
let p be DTree-yielding FinSequence; :: thesis: for i being Element of NAT
for T being DecoratedTree
for q being Node of T st i < len p & T = p . (i + 1) holds
(x -tree p) . (<*i*> ^ q) = T . q
let n be Element of NAT ; :: thesis: for T being DecoratedTree
for q being Node of T st n < len p & T = p . (n + 1) holds
(x -tree p) . (<*n*> ^ q) = T . q
let T be DecoratedTree; :: thesis: for q being Node of T st n < len p & T = p . (n + 1) holds
(x -tree p) . (<*n*> ^ q) = T . q
let q be Node of T; :: thesis: ( n < len p & T = p . (n + 1) implies (x -tree p) . (<*n*> ^ q) = T . q )
assume A1: ( n < len p & T = p . (n + 1) ) ; :: thesis: (x -tree p) . (<*n*> ^ q) = T . q
then A2: <*n*> ^ q in dom (x -tree p) by Th11;
then ( <*n*> in dom (x -tree p) & <*n*> ^ q in tree (doms p) ) by Th10, TREES_1:46;
then q in (dom (x -tree p)) | <*n*> by A2, TREES_1:def 9;
then ( ((x -tree p) | <*n*>) . q = (x -tree p) . (<*n*> ^ q) & T = (x -tree p) | <*n*> ) by A1, Def4, TREES_2:def 11;
hence (x -tree p) . (<*n*> ^ q) = T . q ; :: thesis: verum