for a being object
for i being Nat
for xi, w being FinSequence of NAT
for p, q being DTree-yielding FinSequence
for d, t being DecoratedTree st i < len p & xi = <*i*> ^ w & d = p . (i + 1) & q = p +* ((i + 1),(d with-replacement (w,t))) & xi in tree (doms p) holds
(a -tree p) with-replacement (xi,t) = a -tree q