let x be object ; :: thesis: for p being DTree-yielding FinSequence
for i being 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 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 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
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A2: <*n*> ^ q in dom (x -tree p) by Th11, A1;
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