let T, T9 be DecoratedTree; :: thesis: for p being Element of dom T holds (T with-replacement p,T9) . p = T9 . {}
let p be Element of dom T; :: thesis: (T with-replacement p,T9) . p = T9 . {}
p in (dom T) with-replacement p,(dom T9) by TREES_1:def 12;
then A1: ex r being FinSequence of NAT st
( r in dom T9 & p = p ^ r & (T with-replacement p,T9) . p = T9 . r ) by TREES_2:def 12;
p = p ^ {} by FINSEQ_1:47;
hence (T with-replacement p,T9) . p = T9 . {} by A1, FINSEQ_1:46; :: thesis: verum