theorem Th124: :: MSAFREE5:6

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