theorem :: TREES_3:46

for T, T9 being DecoratedTree
for p being Element of dom T
for q being Element of dom T9 holds (T with-replacement (p,T9)) . (p ^ q) = T9 . q