for i being Nat
for j being Element of NAT st j < i holds
(elementary_tree i) | <*j*> = elementary_tree 0