theorem Th11: :: PRE_CIRC:12

for p being Tree-yielding FinSequence
for k being Element of NAT st k + 1 in dom p holds
(tree p) | <*k*> = p . (k + 1)