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

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