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