for b being object
for c being set
for d being DecoratedTree
for p, q being non empty DTree-yielding FinSequence st dom q = dom p & ( for i being Nat
for d1 being DecoratedTree st i in dom p & d1 = p . i holds
q . i = (d1,c) <- d ) holds
((b -tree p),c) <- d = b -tree q