let i be Nat; :: thesis:
let xi, w be FinSequence of NAT ; :: thesis:
let p, q be Tree-yielding FinSequence; :: thesis:
let d, t be Tree; :: thesis:
assume Z0: i < len p ; :: thesis:
assume Z1: xi = <*i*> ^ w ; :: thesis:
assume Z2: d = p . (i + 1) ; :: thesis:
assume Z3: q = p +* ((i + 1),(d with-replacement (w,t))) ; :: thesis:
assume Z4: xi in tree p ; :: thesis:
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:

hereby :: thesis:

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

per cases by Z4, TREES_1:def 9;

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

per cases by TREES_3:def 15;

suppose n = {} ; :: thesis:

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

end;

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

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

per cases ;

suppose j + 1 <> i + 1 ; :: thesis:

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:

end;

suppose B1: j = i ; :: thesis:

( 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:

end;

end;

end;

end;

end;

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

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:

end;

end;

end;

assume n in tree q ; :: thesis:

per cases by TREES_3:def 15;

suppose n = {} ; :: thesis:

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

end;

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

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

per cases ;

suppose C5: i + 1 <> j + 1 ; :: thesis:

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:

end;

suppose C4: i = j ; :: thesis:

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

per cases by A2, A3, Z2, TREES_1:def 9;

suppose ( u in d & not w c< u ) ; :: thesis:

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:

end;

suppose ex r being FinSequence of NAT st
( r in t & u = w ^ r ) ; :: thesis:

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:

end;

end;

end;

end;

end;

end;