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 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 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 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:25;
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 :: thesis: for s being FinSequence of NAT holds
( ( 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 s in tree q ) )

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 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:22; :: thesis: verum

end;

suppose ex n being 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 Nat, r being FinSequence such that
A8: n < len q and
A9: r in q . (n + 1) and
A10: s = <*n*> ^ r ;

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

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:36;
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:25;
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 ;
then ex s1 being FinSequence st s = <*k*> ^ s1 by TREES_1:1;
then k = s . 1 by FINSEQ_1:41
.= n by A10, FINSEQ_1:41 ;
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 :: thesis: s in tree q

per cases ( s = {} or ex n being 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:22; :: thesis: verum

end;

suppose ex n being 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 Nat, r being FinSequence such that
A16: n < len p and
A17: r in p . (n + 1) and
A18: s = <*n*> ^ r ;

now :: thesis: s in tree q

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:25;
then q . (n + 1) is Tree by TREES_3:22;
then r in q . (n + 1) by A19, TREES_1:22;
hence s in tree q by A1, A16, A18, TREES_3:def 15; :: thesis: verum

end;

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

then A20: n <> k by A15, A18, FINSEQ_1:87, TREES_1:1;
( 1 <= n + 1 & n + 1 <= len p ) by A16, NAT_1:11, NAT_1:13;
then n + 1 in dom p by FINSEQ_3:25;
then q . (n + 1) = p . (n + 1) by A3, A20, 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:22;
then A21: {} in p . (k + 1) by TREES_1:22;
<*k*> = <*k*> ^ {} by FINSEQ_1:34;
then <*k*> in tree p by A4, A21, TREES_3:def 15;
hence tree q = (tree p) with-replacement (<*k*>,t) by A6, TREES_1:def 9; :: thesis: verum