let p, q be Tree-yielding FinSequence; :: thesis: for k being Element of NAT st len p = len q & k + 1 in dom p & ( for i being Element of NAT st i in dom p & i <> k + 1 holds
p . i = q . i ) holds
for t being Tree st q . (k + 1) = t holds
tree q = (tree p) with-replacement (<*k*>,t)
let k be Element of NAT ; :: thesis: ( len p = len q & k + 1 in dom p & ( for i being Element of NAT st i in dom p & i <> k + 1 holds
p . i = q . i ) implies for t being Tree st q . (k + 1) = t holds
tree q = (tree p) with-replacement (<*k*>,t) )
assume that
A1: len p = len q and
A2: k + 1 in dom p and
A3: for i being Element of NAT st i in dom p & i <> k + 1 holds
p . i = q . i ; :: thesis: for t being Tree st q . (k + 1) = t holds
tree q = (tree p) with-replacement (<*k*>,t)
let t be Tree; :: thesis: ( q . (k + 1) = t implies tree q = (tree p) with-replacement (<*k*>,t) )
set o = <*k*>;
k + 1 <= len p by A2, FINSEQ_3:27;
then A4: k < len p by NAT_1:13;
assume A5: q . (k + 1) = t ; :: thesis: tree q = (tree p) with-replacement (<*k*>,t)

A6: now

let s be FinSequence of NAT ; :: thesis: ( ( not s in tree q or ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st
( r in t & s = <*k*> ^ r ) ) & ( ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st
( r in t & s = <*k*> ^ r ) ) implies b₁ in tree q ) )

hereby :: thesis: ( ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st
( r in t & s = <*k*> ^ r ) ) implies b₁ in tree q )

assume A7: s in tree q ; :: thesis: ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st
( r in t & s = <*k*> ^ r ) )

per cases ( s = {} or ex n being Element of NAT ex r being FinSequence st
( n < len q & r in q . (n + 1) & s = <*n*> ^ r ) ) by A7, TREES_3:def 15;

suppose s = {} ; :: thesis: ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st
( r in t & s = <*k*> ^ r ) )

hence ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st
( r in t & s = <*k*> ^ r ) ) by TREES_1:47, XBOOLE_1:115; :: thesis: verum

end;

suppose ex n being Element of NAT ex r being FinSequence st
( n < len q & r in q . (n + 1) & s = <*n*> ^ r ) ; :: thesis: ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st
( r in t & s = <*k*> ^ r ) )

then consider n being Element of NAT , r being FinSequence such that
A8: n < len q and
A9: r in q . (n + 1) and
A10: s = <*n*> ^ r ;

now

per cases ( n = k or n <> k ) ;

case A11: n = k ; :: thesis: ex r being FinSequence of NAT st
( r in t & s = <*k*> ^ r )

reconsider r = r as FinSequence of NAT by A10, FINSEQ_1:50;
take r = r; :: thesis: ( r in t & s = <*k*> ^ r )
thus ( r in t & s = <*k*> ^ r ) by A5, A9, A10, A11; :: thesis: verum

end;

case A12: n <> k ; :: thesis: ( s in tree p & not <*k*> is_a_proper_prefix_of s )

( 1 <= n + 1 & n + 1 <= len p ) by A1, A8, NAT_1:11, NAT_1:13;
then n + 1 in dom p by FINSEQ_3:27;
then q . (n + 1) = p . (n + 1) by A3, A12, XCMPLX_1:2;
hence s in tree p by A1, A8, A9, A10, TREES_3:def 15; :: thesis: not <*k*> is_a_proper_prefix_of s
assume <*k*> is_a_proper_prefix_of s ; :: thesis: contradiction
then <*k*> is_a_prefix_of s by XBOOLE_0:def 8;
then ex s1 being FinSequence st s = <*k*> ^ s1 by TREES_1:8;
then k = s . 1 by FINSEQ_1:58
.= n by A10, FINSEQ_1:58 ;
hence contradiction by A12; :: thesis: verum

end;

end;

end;

hence ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st
( r in t & s = <*k*> ^ r ) ) ; :: thesis: verum

end;

end;

end;

assume A13: ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st
( r in t & s = <*k*> ^ r ) ) ; :: thesis: b₁ in tree q

per cases ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st
( r in t & s = <*k*> ^ r ) ) by A13;

suppose that A14: s in tree p and
A15: not <*k*> is_a_proper_prefix_of s ; :: thesis: b₁ in tree q

now

per cases ( s = {} or ex n being Element of NAT ex r being FinSequence st
( n < len p & r in p . (n + 1) & s = <*n*> ^ r ) ) by A14, TREES_3:def 15;

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

hence s in tree q by TREES_1:47; :: thesis: verum

end;

suppose ex n being Element of NAT ex r being FinSequence st
( n < len p & r in p . (n + 1) & s = <*n*> ^ r ) ; :: thesis: s in tree q

then consider n being Element of NAT , r being FinSequence such that
A16: n < len p and
A17: r in p . (n + 1) and
A18: s = <*n*> ^ r ;

now

per cases ( r = {} or r <> {} ) ;

suppose A19: r = {} ; :: thesis: s in tree q

( 1 <= n + 1 & n + 1 <= len q ) by A1, A16, NAT_1:11, NAT_1:13;
then n + 1 in dom q by FINSEQ_3:27;
then q . (n + 1) is Tree by TREES_3:24;
then r in q . (n + 1) by A19, TREES_1:47;
hence s in tree q by A1, A16, A18, TREES_3:def 15; :: thesis: verum

end;

suppose A20: r <> {} ; :: thesis: s in tree q

A21: now

assume n = k ; :: thesis: contradiction
then ( <*k*> is_a_prefix_of s & not s = <*k*> ) by A18, A20, FINSEQ_1:108, TREES_1:8;
hence contradiction by A15, XBOOLE_0:def 8; :: thesis: verum

end;

( 1 <= n + 1 & n + 1 <= len p ) by A16, NAT_1:11, NAT_1:13;
then n + 1 in dom p by FINSEQ_3:27;
then q . (n + 1) = p . (n + 1) by A3, A21, XCMPLX_1:2;
hence s in tree q by A1, A16, A17, A18, TREES_3:def 15; :: thesis: verum

end;

end;

end;

hence s in tree q ; :: thesis: verum

end;

end;

end;

hence s in tree q ; :: thesis: verum

end;

suppose ex r being FinSequence of NAT st
( r in t & s = <*k*> ^ r ) ; :: thesis: b₁ in tree q

hence s in tree q by A1, A4, A5, TREES_3:def 15; :: thesis: verum

end;

end;

end;

p . (k + 1) is Tree by A2, TREES_3:24;
then A22: {} in p . (k + 1) by TREES_1:47;
<*k*> = <*k*> ^ {} by FINSEQ_1:47;
then <*k*> in tree p by A4, A22, TREES_3:def 15;
hence tree q = (tree p) with-replacement (<*k*>,t) by A6, TREES_1:def 12; :: thesis: verum