theorem :: TREES_3:44

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