theorem :: TREES_9:31

for t being finite-branching DecoratedTree
for p being Node of t
for q being Node of (t | p) holds succ (t,(p ^ q)) = succ ((t | p),q)