for p being FinSequence st p is Tree-yielding holds
( (tree p) -level 1 = { <*n*> where n is Nat : n < len p } & ( for n being Element of NAT st n < len p holds
(tree p) | <*n*> = p . (n + 1) ) )