theorem :: TREES_3:56

for p being Tree-yielding FinSequence holds tree (p ^ <*(elementary_tree 0)*>) = (tree p) \/ (elementary_tree ((len p) + 1))