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 9;
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 11;
p = p ^ {} by FINSEQ_1:34;
hence (T with-replacement (p,T9)) . p = T9 . {} by A1, FINSEQ_1:33; :: thesis: verum