let i be Nat; :: thesis: for xi, w being FinSequence of NAT
for p, q being Tree-yielding FinSequence
for d, t being Tree st i < len p & xi = <*i*> ^ w & d = p . (i + 1) & q = p +* ((i + 1),(d with-replacement (w,t))) & xi in tree p holds
(tree p) with-replacement (xi,t) = tree q
let xi, w be FinSequence of NAT ; :: thesis: for p, q being Tree-yielding FinSequence
for d, t being Tree st i < len p & xi = <*i*> ^ w & d = p . (i + 1) & q = p +* ((i + 1),(d with-replacement (w,t))) & xi in tree p holds
(tree p) with-replacement (xi,t) = tree q
let p, q be Tree-yielding FinSequence; :: thesis: for d, t being Tree st i < len p & xi = <*i*> ^ w & d = p . (i + 1) & q = p +* ((i + 1),(d with-replacement (w,t))) & xi in tree p holds
(tree p) with-replacement (xi,t) = tree q
let d, t be Tree; :: thesis: ( i < len p & xi = <*i*> ^ w & d = p . (i + 1) & q = p +* ((i + 1),(d with-replacement (w,t))) & xi in tree p implies (tree p) with-replacement (xi,t) = 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 p or (tree p) with-replacement (xi,t) = 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 p or (tree p) with-replacement (xi,t) = tree q )
assume Z2: d = p . (i + 1) ; :: thesis: ( not q = p +* ((i + 1),(d with-replacement (w,t))) or not xi in tree p or (tree p) with-replacement (xi,t) = tree q )
assume Z3: q = p +* ((i + 1),(d with-replacement (w,t))) ; :: thesis: ( not xi in tree p or (tree p) with-replacement (xi,t) = tree q )
assume Z4: xi in tree p ; :: thesis: (tree p) with-replacement (xi,t) = tree q
consider j being Nat, u being FinSequence such that
A2: ( j < len p & u in 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;
dom p = dom q by Z3, FUNCT_7:30;
then A4: len p = len q by FINSEQ_3:29;
( 1 <= i + 1 & i + 1 <= len p ) by Z0, NAT_1:12, NAT_1:13;
then AA: i + 1 in dom p by FINSEQ_3:25;
then A7: q . (i + 1) = d with-replacement (w,t) by Z3, FUNCT_7:31;
let n be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not n in (tree p) with-replacement (xi,t) or n in tree q ) & ( not n in tree q or n in (tree p) with-replacement (xi,t) ) )

hereby :: thesis: ( not n in tree q or n in (tree p) with-replacement (xi,t) )

assume n in (tree p) with-replacement (xi,t) ; :: thesis: n in tree q

per cases then ( ( n in tree p & not xi is_a_proper_prefix_of n ) or ex r being FinSequence of NAT st
( r in t & n = xi ^ r ) ) by Z4, TREES_1:def 9;

suppose A8: ( n in tree p & not xi is_a_proper_prefix_of n ) ; :: thesis: n in tree q

per cases then ( n = {} or ex j being Nat ex u being FinSequence st
( j < len p & u in p . (j + 1) & n = <*j*> ^ u ) ) by TREES_3:def 15;

suppose n = {} ; :: thesis: n in tree q

hence n in tree q by TREES_1:22; :: thesis: verum

end;

suppose ex j being Nat ex u being FinSequence st
( j < len p & u in p . (j + 1) & n = <*j*> ^ u ) ; :: thesis: n in tree q

then consider j being Nat, u being FinSequence such that
A9: ( j < len p & u in p . (j + 1) & n = <*j*> ^ u ) ;

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

suppose j + 1 <> i + 1 ; :: thesis: n in tree q

then q . (j + 1) = p . (j + 1) by Z3, FUNCT_7:32;
hence n in tree q by A4, A9, TREES_3:def 15; :: thesis: verum

end;

suppose B1: j = i ; :: thesis: n in tree q

( xi = n or not xi c= n ) by A8, XBOOLE_0:def 8;
then B2: not w is_a_proper_prefix_of u by Z1, A9, B1, HILBERT2:2, FINSEQ_6:13, XBOOLE_0:def 8;
u is Element of d by Z2, A9, B1;
then u in d with-replacement (w,t) by A2, A3, Z2, B2, TREES_1:def 9;
hence n in tree q by A4, A7, A9, B1, TREES_3:def 15; :: thesis: verum

end;

end;

end;

end;

end;

suppose ex r being FinSequence of NAT st
( r in t & n = xi ^ r ) ; :: thesis: n in tree q

then consider r being FinSequence of NAT such that
A1: ( r in t & n = xi ^ r ) ;
w ^ r in d with-replacement (w,t) by A1, A2, A3, Z2, TREES_1:def 9;
then <*i*> ^ (w ^ r) in tree q by Z0, A4, A7, TREES_3:def 15;
hence n in tree q by Z1, A1, FINSEQ_1:32; :: thesis: verum

end;

end;

end;

assume n in tree q ; :: thesis: n in (tree p) with-replacement (xi,t)

per cases then ( n = {} or ex i being Nat ex w being FinSequence st
( i < len q & w in q . (i + 1) & n = <*i*> ^ w ) ) by TREES_3:def 15;

suppose n = {} ; :: thesis: n in (tree p) with-replacement (xi,t)

hence n in (tree p) with-replacement (xi,t) by TREES_1:22; :: thesis: verum

end;

suppose ex i being Nat ex w being FinSequence st
( i < len q & w in q . (i + 1) & n = <*i*> ^ w ) ; :: thesis: n in (tree p) with-replacement (xi,t)

then consider j being Nat, u being FinSequence such that
C1: ( j < len q & u in q . (j + 1) & n = <*j*> ^ u ) ;

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

suppose C5: i + 1 <> j + 1 ; :: thesis: n in (tree p) with-replacement (xi,t)

then ( q . (j + 1) = p . (j + 1) & i <> j ) by Z3, FUNCT_7:32;
then C3: n in tree p by A4, C1, TREES_3:def 15;
not <*i*> c= <*j*> ^ u by C5, TREES_1:50;
then not xi c< n by Z1, C1, Lem8, XBOOLE_0:def 8;
hence n in (tree p) with-replacement (xi,t) by Z4, C3, TREES_1:def 9; :: thesis: verum

end;

suppose C4: i = j ; :: thesis: n in (tree p) with-replacement (xi,t)

then reconsider u = u as Element of d with-replacement (w,t) by AA, C1, Z3, FUNCT_7:31;

per cases ( ( u in d & not w c< u ) or ex r being FinSequence of NAT st
( r in t & u = w ^ r ) ) by A2, A3, Z2, TREES_1:def 9;

suppose ( u in d & not w c< u ) ; :: thesis: n in (tree p) with-replacement (xi,t)

then ( n in tree p & not xi c< n ) by Z1, Z2, A4, C1, C4, TREES_1:49, TREES_3:def 15;
hence n in (tree p) with-replacement (xi,t) by Z4, TREES_1:def 9; :: thesis: verum

end;

suppose ex r being FinSequence of NAT st
( r in t & u = w ^ r ) ; :: thesis: n in (tree p) with-replacement (xi,t)

then consider r being FinSequence of NAT such that
C5: ( r in t & u = w ^ r ) ;
n = xi ^ r by Z1, C1, C4, C5, FINSEQ_1:32;
hence n in (tree p) with-replacement (xi,t) by Z4, C5, TREES_1:def 9; :: thesis: verum

end;

end;

end;

end;

end;

end;