theorem Th3: :: TREES_9:3

for t being DecoratedTree
for p, q being FinSequence of NAT st p ^ q in dom t holds
t | (p ^ q) = (t | p) | q