let t, t1 be DecoratedTree; :: thesis: for xi being Node of t holds (t with-replacement (xi,t1)) | xi = t1
let xi be Node of t; :: thesis: (t with-replacement (xi,t1)) | xi = t1
A1: ( xi in (dom t) with-replacement (xi,(dom t1)) & (dom t) with-replacement (xi,(dom t1)) = dom (t with-replacement (xi,t1)) ) by TREES_1:def 9, TREES_2:def 11;
A2: dom ((t with-replacement (xi,t1)) | xi) = (dom (t with-replacement (xi,t1))) | xi by TREES_2:def 10;
hence dom ((t with-replacement (xi,t1)) | xi) = dom t1 by A1, Th129; :: according to TREES_4:def 1 :: thesis: for b₁ being Element of proj1 ((t with-replacement (xi,t1)) | xi) holds ((t with-replacement (xi,t1)) | xi) . b₁ = t1 . b₁
let p be Node of ((t with-replacement (xi,t1)) | xi); :: thesis: ((t with-replacement (xi,t1)) | xi) . p = t1 . p
( xi ^ p in dom (t with-replacement (xi,t1)) & xi c= xi ^ p ) by A1, A2, TREES_1:1, TREES_1:def 6;
then consider r being FinSequence of NAT such that
A4: ( r in dom t1 & xi ^ p = xi ^ r & (t with-replacement (xi,t1)) . (xi ^ p) = t1 . r ) by A1, TREES_2:def 11;
thus ((t with-replacement (xi,t1)) | xi) . p = (t with-replacement (xi,t1)) . (xi ^ p) by A2, TREES_2:def 10
.= t1 . p by A4, FINSEQ_1:33 ; :: thesis: verum