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) by TREES_1:21;
then q in (dom (x -tree p)) | <*n*> by A2, TREES_1:def 6;
then ((x -tree p) | <*n*>) . q = (x -tree p) . (<*n*> ^ q) by TREES_2:def 10;
hence (x -tree p) . (<*n*> ^ q) = T . q by A1, Def4; :: thesis: verum