theorem :: PRE_CIRC:15

for e1, e2 being finite DecoratedTree
for x being set
for k being Element of NAT
for p being DTree-yielding FinSequence st <*k*> in dom e1 & e1 = x -tree p holds
ex q being DTree-yielding FinSequence st
( e1 with-replacement (<*k*>,e2) = x -tree q & len q = len p & q . (k + 1) = e2 & ( for i being Nat st i in dom p & i <> k + 1 holds
q . i = p . i ) )