theorem Th13: :: TREES_A:13

for p being FinSequence of NAT
for T, T1 being DecoratedTree st p in dom T holds
for q being FinSequence of NAT st q in dom (T with-replacement (p,T1)) & q in { t1 where t1 is Element of dom T : not p is_a_prefix_of t1 } holds
(T with-replacement (p,T1)) . q = T . q