let x be object ; :: thesis: for p being FinSequence
for i being Element of NAT st i < len p holds
(x -flat_tree p) | <*i*> = root-tree (p . (i + 1))
let p be FinSequence; :: thesis: for i being Element of NAT st i < len p holds
(x -flat_tree p) | <*i*> = root-tree (p . (i + 1))
let i be Element of NAT ; :: thesis: ( i < len p implies (x -flat_tree p) | <*i*> = root-tree (p . (i + 1)) )
reconsider t = {} as Element of (dom (x -flat_tree p)) | <*i*> by TREES_1:22;
assume A1: i < len p ; :: thesis: (x -flat_tree p) | <*i*> = root-tree (p . (i + 1))
then A2: (x -flat_tree p) . <*i*> = p . (i + 1) by Def3;
A3: dom (x -flat_tree p) = elementary_tree (len p) by Def3;
(elementary_tree (len p)) | <*i*> = elementary_tree 0 by A1, Th8;
then A4: dom ((x -flat_tree p) | <*i*>) = elementary_tree 0 by A3, TREES_2:def 10;
( <*i*> ^ t = <*i*> & ((x -flat_tree p) | <*i*>) . t = (x -flat_tree p) . (<*i*> ^ t) ) by FINSEQ_1:34, TREES_2:def 10;
hence (x -flat_tree p) | <*i*> = root-tree (p . (i + 1)) by A2, A4, Th5; :: thesis: verum