let t, t1 be DecoratedTree; for xi, nu being Node of t st not xi c= nu & not nu c= xi holds
(t with-replacement (xi,t1)) | nu = t | nu
let xi, nu be Node of t; ( not xi c= nu & not nu c= xi implies (t with-replacement (xi,t1)) | nu = t | nu )
assume Z0:
not xi c= nu
; ( nu c= xi or (t with-replacement (xi,t1)) | nu = t | nu )
assume Z1:
not nu c= xi
; (t with-replacement (xi,t1)) | nu = t | nu
not xi c< nu
by Z0, XBOOLE_0:def 8;
then A1:
( nu 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)) | nu) = (dom (t with-replacement (xi,t1))) | nu
by TREES_2:def 10;
hence A4: dom ((t with-replacement (xi,t1)) | nu) =
(dom t) | nu
by Z0, Z1, A1, Th134
.=
dom (t | nu)
by TREES_2:def 10
;
TREES_4:def 1 for b1 being Element of proj1 ((t with-replacement (xi,t1)) | nu) holds ((t with-replacement (xi,t1)) | nu) . b1 = (t | nu) . b1
let p be Node of ((t with-replacement (xi,t1)) | nu); ((t with-replacement (xi,t1)) | nu) . p = (t | nu) . p
A8:
(dom t) | nu = dom (t | nu)
by TREES_2:def 10;
then A5:
( nu ^ p in dom t & (t | nu) . p = t . (nu ^ p) )
by A4, TREES_1:def 6, TREES_2:def 10;
not xi c< nu ^ p
by Z0, Z1, Lem8B, XBOOLE_0:def 8;
then A7:
nu ^ p in (dom t) with-replacement (xi,(dom t1))
by A5, TREES_1:def 9;
A6:
for r being FinSequence of NAT holds
( not r in dom t1 or not nu ^ p = xi ^ r or not (t with-replacement (xi,t1)) . (nu ^ p) = t1 . r )
by Z0, Z1, Lem8B, TREES_1:1;
thus ((t with-replacement (xi,t1)) | nu) . p =
(t with-replacement (xi,t1)) . (nu ^ p)
by A2, TREES_2:def 10
.=
t . (nu ^ p)
by A6, A7, TREES_2:def 11
.=
(t | nu) . p
by A8, TREES_2:def 10, A4
; verum