for p, q being Tree-yielding FinSequence
for k being Element of NAT st len p = len q & k + 1 in dom p & ( for i being Nat st i in dom p & i <> k + 1 holds
p . i = q . i ) holds
for t being Tree st q . (k + 1) = t holds
tree q = (tree p) with-replacement (<*k*>,t)