let p, q be Tree-yielding FinSequence; :: thesis:
let k be Element of NAT ; :: thesis:
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:
let t be Tree; :: thesis:
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:

A6: now :: thesis:

let s be FinSequence of NAT ; :: thesis:

hereby :: thesis:

assume A7: s in tree q ; :: thesis:

per cases by A7, TREES_3:def 15;

suppose s = {} ; :: thesis:

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:

end;

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

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 ;

case A11: n = k ; :: thesis:

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

end;

case A12: n <> k ; :: thesis:

( 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:
assume <*k*> is_a_proper_prefix_of s ; :: thesis:
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:

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:

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:

per cases by A13;

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

per cases by A14, TREES_3:def 15;

suppose s = {} ; :: thesis:

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

end;

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

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 ;

suppose A19: r = {} ; :: thesis:

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

end;

suppose r <> {} ; :: thesis:

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:

end;

end;

end;

hence s in tree q ; :: thesis:

end;

end;

end;

hence s in tree q ; :: thesis:

end;

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

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

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: