let a be object ; :: thesis: for i being Nat
for xi, w being FinSequence of NAT
for p, q being DTree-yielding FinSequence
for d, t being DecoratedTree st i < len p & xi = <*i*> ^ w & d = p . (i + 1) & q = p +* ((i + 1),(d with-replacement (w,t))) & xi in tree (doms p) holds
(a -tree p) with-replacement (xi,t) = a -tree q
let i be Nat; :: thesis: for xi, w being FinSequence of NAT
for p, q being DTree-yielding FinSequence
for d, t being DecoratedTree st i < len p & xi = <*i*> ^ w & d = p . (i + 1) & q = p +* ((i + 1),(d with-replacement (w,t))) & xi in tree (doms p) holds
(a -tree p) with-replacement (xi,t) = a -tree q
let xi, w be FinSequence of NAT ; :: thesis: for p, q being DTree-yielding FinSequence
for d, t being DecoratedTree st i < len p & xi = <*i*> ^ w & d = p . (i + 1) & q = p +* ((i + 1),(d with-replacement (w,t))) & xi in tree (doms p) holds
(a -tree p) with-replacement (xi,t) = a -tree q
let p, q be DTree-yielding FinSequence; :: thesis: for d, t being DecoratedTree st i < len p & xi = <*i*> ^ w & d = p . (i + 1) & q = p +* ((i + 1),(d with-replacement (w,t))) & xi in tree (doms p) holds
(a -tree p) with-replacement (xi,t) = a -tree q
let d, t be DecoratedTree; :: thesis: ( i < len p & xi = <*i*> ^ w & d = p . (i + 1) & q = p +* ((i + 1),(d with-replacement (w,t))) & xi in tree (doms p) implies (a -tree p) with-replacement (xi,t) = a -tree q )
assume Z0: i < len p ; :: thesis: ( not xi = <*i*> ^ w or not d = p . (i + 1) or not q = p +* ((i + 1),(d with-replacement (w,t))) or not xi in tree (doms p) or (a -tree p) with-replacement (xi,t) = a -tree q )
assume Z1: xi = <*i*> ^ w ; :: thesis: ( not d = p . (i + 1) or not q = p +* ((i + 1),(d with-replacement (w,t))) or not xi in tree (doms p) or (a -tree p) with-replacement (xi,t) = a -tree q )
assume Z2: d = p . (i + 1) ; :: thesis: ( not q = p +* ((i + 1),(d with-replacement (w,t))) or not xi in tree (doms p) or (a -tree p) with-replacement (xi,t) = a -tree q )
assume Z3: q = p +* ((i + 1),(d with-replacement (w,t))) ; :: thesis: ( not xi in tree (doms p) or (a -tree p) with-replacement (xi,t) = a -tree q )
assume Z4: xi in tree (doms p) ; :: thesis: (a -tree p) with-replacement (xi,t) = a -tree q
A1: ( dom (a -tree p) = tree (doms p) & dom (a -tree q) = tree (doms q) ) by TREES_4:10;
AA: doms q = (doms p) +* ((i + 1),(dom (d with-replacement (w,t)))) by Z3, Lem12;
consider j being Nat, u being FinSequence such that
A2: ( j < len (doms p) & u in (doms p) . (j + 1) & xi = <*j*> ^ u ) by Z1, Z4, TREES_3:def 15;
A3: ( i = xi . 1 & xi . 1 = j & w = u ) by Z1, A2, FINSEQ_1:41, HILBERT2:2;
( 1 <= i + 1 & i + 1 <= len p ) by Z0, NAT_1:12, NAT_1:13;
then i + 1 in dom p by FINSEQ_3:25;
then A4: ( w in dom d & dom d = (doms p) . (i + 1) ) by Z2, A2, A3, FUNCT_6:def 2;
then dom (d with-replacement (w,t)) = (dom d) with-replacement (w,(dom t)) by TREES_2:def 11;
then A5: ( dom ((a -tree p) with-replacement (xi,t)) = (tree (doms p)) with-replacement (xi,(dom t)) & (tree (doms p)) with-replacement (xi,(dom t)) = tree (doms q) ) by Z4, A1, AA, A2, A3, A4, Th124, TREES_2:def 11;
hence dom ((a -tree p) with-replacement (xi,t)) = dom (a -tree q) by TREES_4:10; :: according to TREES_4:def 1 :: thesis: for b₁ being Element of proj1 ((a -tree p) with-replacement (xi,t)) holds ((a -tree p) with-replacement (xi,t)) . b₁ = (a -tree q) . b₁
A8: ( dom (doms q) = dom q & dom q = dom p & dom p = dom (doms p) ) by Z3, FUNCT_6:def 2, FUNCT_7:30;
then A7: ( len (doms q) = len q & len q = len p & len p = len (doms p) ) by FINSEQ_3:29;
let nu be Element of dom ((a -tree p) with-replacement (xi,t)); :: thesis: ((a -tree p) with-replacement (xi,t)) . nu = (a -tree q) . nu

per cases ( nu = {} or ex j being Nat ex r being FinSequence st
( j < len (doms q) & r in (doms q) . (j + 1) & nu = <*j*> ^ r ) ) by A5, TREES_3:def 15;

suppose A6: nu = {} ; :: thesis: ((a -tree p) with-replacement (xi,t)) . nu = (a -tree q) . nu

then for r being FinSequence of NAT holds
( not r in dom t or not nu = xi ^ r or not ((a -tree p) with-replacement (xi,t)) . nu = t . r ) by Z1;
hence ((a -tree p) with-replacement (xi,t)) . nu = (a -tree p) . nu by Z4, A1, A5, TREES_2:def 11
.= a by A6, TREES_4:def 4
.= (a -tree q) . nu by A6, TREES_4:def 4 ;
:: thesis: verum

end;

suppose ex j being Nat ex r being FinSequence st
( j < len (doms q) & r in (doms q) . (j + 1) & nu = <*j*> ^ r ) ; :: thesis: ((a -tree p) with-replacement (xi,t)) . nu = (a -tree q) . nu

then consider j being Nat, r being FinSequence such that
A6: ( j < len (doms q) & r in (doms q) . (j + 1) & nu = <*j*> ^ r ) ;
AB: ( 1 <= j + 1 & j + 1 <= len p ) by A6, A7, NAT_1:12, NAT_1:13;
then A9: j + 1 in dom p by FINSEQ_3:25;

per cases ( j <> i or j = i ) ;

suppose A10: j <> i ; :: thesis: ((a -tree p) with-replacement (xi,t)) . nu = (a -tree q) . nu

then j + 1 <> i + 1 ;
then A11: ( dom (q . (j + 1)) = (doms q) . (j + 1) & (doms q) . (j + 1) = (doms p) . (j + 1) & (doms p) . (j + 1) = dom (p . (j + 1)) & q . (j + 1) = p . (j + 1) ) by Z3, AA, A8, AB, FINSEQ_3:25, FUNCT_7:32, FUNCT_6:def 2;
reconsider t1 = p . (j + 1) as DecoratedTree by A9, TREES_3:24;
not xi c= nu by A6, Z1, Lem8, A10, TREES_1:50;
then for r being FinSequence of NAT holds
( not r in dom t or not nu = xi ^ r or not ((a -tree p) with-replacement (xi,t)) . nu = t . r ) by TREES_1:1;
hence ((a -tree p) with-replacement (xi,t)) . nu = (a -tree p) . nu by Z4, A1, A5, TREES_2:def 11
.= t1 . r by A6, A7, A11, TREES_4:12
.= (a -tree q) . nu by A6, A7, A11, TREES_4:12 ;
:: thesis: verum

end;

suppose A10: j = i ; :: thesis: ((a -tree p) with-replacement (xi,t)) . nu = (a -tree q) . nu

then A11: ( dom (q . (j + 1)) = (doms q) . (j + 1) & (doms p) . (j + 1) = dom (p . (j + 1)) & q . (j + 1) = d with-replacement (w,t) ) by Z3, A8, AB, FINSEQ_3:25, FUNCT_7:31, FUNCT_6:def 2;
then reconsider r = r as Element of (dom d) with-replacement (w,(dom t)) by A6, Z2, A2, A3, A10, TREES_2:def 11;

per cases ( w c= r or not w c= r ) ;

suppose A12: w c= r ; :: thesis: ((a -tree p) with-replacement (xi,t)) . nu = (a -tree q) . nu

then consider r2 being FinSequence of NAT such that
A13: ( r2 in dom t & r = w ^ r2 & (d with-replacement (w,t)) . r = t . r2 ) by Z2, A2, A3, A10, A11, TREES_2:def 11;
xi c= nu by Z1, A6, A10, A12, FINSEQ_6:13;
then consider r3 being FinSequence of NAT such that
A15: ( r3 in dom t & nu = xi ^ r3 & ((a -tree p) with-replacement (xi,t)) . nu = t . r3 ) by Z4, A5, A1, TREES_2:def 11;
nu = xi ^ r2 by Z1, A6, A10, A13, FINSEQ_1:32;
then ((a -tree p) with-replacement (xi,t)) . nu = t . r2 by A15, FINSEQ_1:33;
hence ((a -tree p) with-replacement (xi,t)) . nu = (a -tree q) . nu by A13, A6, A7, A11, TREES_4:12; :: thesis: verum

end;

suppose A12: not w c= r ; :: thesis: ((a -tree p) with-replacement (xi,t)) . nu = (a -tree q) . nu

then A13: for r2 being FinSequence of NAT holds
( not r2 in dom t or not r = w ^ r2 or not (d with-replacement (w,t)) . r = t . r2 ) by TREES_1:1;
for r2 being FinSequence of NAT holds
( not r2 in dom t or not r = w ^ r2 ) by A12, TREES_1:1;
then A15: r in dom d by Z2, A2, A3, A10, A11, TREES_1:def 9;
for r being FinSequence of NAT holds
( not r in dom t or not nu = xi ^ r or not ((a -tree p) with-replacement (xi,t)) . nu = t . r ) by A12, A10, A6, Z1, Lem8A, TREES_1:1;
hence ((a -tree p) with-replacement (xi,t)) . nu = (a -tree p) . nu by Z4, A1, A5, TREES_2:def 11
.= d . r by Z2, A15, A6, A7, A10, TREES_4:12
.= (d with-replacement (w,t)) . r by A13, A4, TREES_2:def 11
.= (a -tree q) . nu by A6, A7, A11, TREES_4:12 ;
:: thesis: verum

end;

end;

end;

end;

end;

end;