theorem Th9: :: TREES_4:9

for x being object
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))