for T being DecoratedTree
for p being FinSequence of NAT holds T . p = (T | p) . {}