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 ;
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 b1 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 b1 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 ;
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 ;
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 ;
then n + 1 in dom p by FINSEQ_3:25;
then q . (n + 1) = p . (n + 1) by ;
hence s in tree p by ; :: thesis:
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 ;
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: b1 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: b1 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 ;
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 ;
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 ;
hence s in tree q by ; :: thesis: verum
end;
suppose r <> {} ; :: thesis: s in tree q
then A20: n <> k by ;
( 1 <= n + 1 & n + 1 <= len p ) by ;
then n + 1 in dom p by FINSEQ_3:25;
then q . (n + 1) = p . (n + 1) by ;
hence s in tree q by ; :: 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: b1 in tree q
hence s in tree q by ; :: thesis: verum
end;
end;
end;
p . (k + 1) is Tree by ;
then A21: {} in p . (k + 1) by TREES_1:22;
<*k*> = <*k*> ^ {} by FINSEQ_1:34;
then <*k*> in tree p by ;
hence tree q = (tree p) with-replacement (<*k*>,t) by ; :: thesis: verum