let e1, e2 be finite DecoratedTree; :: thesis: for x being set
for k being Element of NAT
for p being DTree-yielding FinSequence st <*k*> in dom e1 & e1 = x -tree p holds
ex q being DTree-yielding FinSequence st
( e1 with-replacement (<*k*>,e2) = x -tree q & len q = len p & q . (k + 1) = e2 & ( for i being Nat st i in dom p & i <> k + 1 holds
q . i = p . i ) )
let x be set ; :: thesis: for k being Element of NAT
for p being DTree-yielding FinSequence st <*k*> in dom e1 & e1 = x -tree p holds
ex q being DTree-yielding FinSequence st
( e1 with-replacement (<*k*>,e2) = x -tree q & len q = len p & q . (k + 1) = e2 & ( for i being Nat st i in dom p & i <> k + 1 holds
q . i = p . i ) )
let k be Element of NAT ; :: thesis: for p being DTree-yielding FinSequence st <*k*> in dom e1 & e1 = x -tree p holds
ex q being DTree-yielding FinSequence st
( e1 with-replacement (<*k*>,e2) = x -tree q & len q = len p & q . (k + 1) = e2 & ( for i being Nat st i in dom p & i <> k + 1 holds
q . i = p . i ) )
let p be DTree-yielding FinSequence; :: thesis: ( <*k*> in dom e1 & e1 = x -tree p implies ex q being DTree-yielding FinSequence st
( e1 with-replacement (<*k*>,e2) = x -tree q & len q = len p & q . (k + 1) = e2 & ( for i being Nat st i in dom p & i <> k + 1 holds
q . i = p . i ) ) )
assume that
A1: <*k*> in dom e1 and
A2: e1 = x -tree p ; :: thesis: ex q being DTree-yielding FinSequence st
( e1 with-replacement (<*k*>,e2) = x -tree q & len q = len p & q . (k + 1) = e2 & ( for i being Nat st i in dom p & i <> k + 1 holds
q . i = p . i ) )
consider j being Nat, T being DecoratedTree, w being Node of T such that
A3: j < len p and
T = p . (j + 1) and
A4: <*k*> = <*j*> ^ w by A1, A2, TREES_4:11;
consider pp being DTree-yielding FinSequence such that
A5: p = pp and
A6: dom (x -tree p) = tree (doms pp) by TREES_4:def 4;
A7: dom (doms pp) = dom p by A5, TREES_3:37;
deffunc H₁( Nat) -> set = IFEQ ($1,(k + 1),e2,(p . $1));
set o = <*k*>;
consider q being FinSequence such that
A8: len q = len p and
A9: for i being Nat st i in dom q holds
q . i = H₁(i) from FINSEQ_1:sch 2();
A10: dom q = Seg (len p) by A8, FINSEQ_1:def 3;
A11: dom q = dom p by A8, FINSEQ_3:29;

now :: thesis: for x being object st x in dom q holds
q . x is DecoratedTree

let x be object ; :: thesis: ( x in dom q implies q . x is DecoratedTree )
assume A12: x in dom q ; :: thesis: q . x is DecoratedTree
then reconsider i = x as Nat ;
A13: ( i = k + 1 or i <> k + 1 ) ;
q . i = IFEQ (i,(k + 1),e2,(p . i)) by A9, A12;
then ( q . i = e2 or q . i = p . i ) by A13, FUNCOP_1:def 8;
hence q . x is DecoratedTree by A11, A12, TREES_3:24; :: thesis: verum

end;

then reconsider q = q as DTree-yielding FinSequence by TREES_3:24;
consider qq being DTree-yielding FinSequence such that
A14: q = qq and
A15: dom (x -tree q) = tree (doms qq) by TREES_4:def 4;
A16: len (doms pp) = len p by A5, TREES_3:38
.= len (doms qq) by A8, A14, TREES_3:38 ;
A17: dom p = Seg (len p) by FINSEQ_1:def 3;

A18: now :: thesis: for i being Nat st i in dom (doms pp) & i <> k + 1 holds
(doms pp) . i = (doms qq) . i

let i be Nat; :: thesis: ( i in dom (doms pp) & i <> k + 1 implies (doms pp) . i = (doms qq) . i )
assume that
A19: i in dom (doms pp) and
A20: i <> k + 1 ; :: thesis: (doms pp) . i = (doms qq) . i
A21: q . i = IFEQ (i,(k + 1),e2,(p . i)) by A9, A10, A17, A7, A19
.= p . i by A20, FUNCOP_1:def 8 ;
reconsider pii = p . i as DecoratedTree by A7, A19, TREES_3:24;
thus (doms pp) . i = dom pii by A5, A7, A19, FUNCT_6:22
.= (doms qq) . i by A11, A14, A7, A19, A21, FUNCT_6:22 ; :: thesis: verum

end;

reconsider dqq = doms qq as Tree-yielding FinSequence ;
take q ; :: thesis: ( e1 with-replacement (<*k*>,e2) = x -tree q & len q = len p & q . (k + 1) = e2 & ( for i being Nat st i in dom p & i <> k + 1 holds
q . i = p . i ) )
<*j*> = <*k*> by A4, FINSEQ_1:88;
then A22: j = <*k*> . 1
.= k ;
then ( 1 <= k + 1 & k + 1 <= len p ) by A3, NAT_1:11, NAT_1:13;
then A23: k + 1 in dom p by FINSEQ_3:25;
then k + 1 in Seg (len p) by FINSEQ_1:def 3;
then A24: q . (k + 1) = IFEQ ((k + 1),(k + 1),e2,(p . (k + 1))) by A9, A10
.= e2 by FUNCOP_1:def 8 ;
then (doms qq) . (k + 1) = dom e2 by A11, A23, A14, FUNCT_6:22;
then A25: dom (x -tree q) = (dom e1) with-replacement (<*k*>,(dom e2)) by A2, A23, A15, A6, A16, A7, A18, Th13;
for f being FinSequence of NAT holds
( not f in (dom e1) with-replacement (<*k*>,(dom e2)) or ( not <*k*> is_a_prefix_of f & (x -tree q) . f = e1 . f ) or ex r being FinSequence of NAT st
( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r ) )

proof

reconsider o9 = <*k*> as Element of dom e1 by A1;
let f be FinSequence of NAT ; :: thesis: ( not f in (dom e1) with-replacement (<*k*>,(dom e2)) or ( not <*k*> is_a_prefix_of f & (x -tree q) . f = e1 . f ) or ex r being FinSequence of NAT st
( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r ) )
assume A26: f in (dom e1) with-replacement (<*k*>,(dom e2)) ; :: thesis: ( ( not <*k*> is_a_prefix_of f & (x -tree q) . f = e1 . f ) or ex r being FinSequence of NAT st
( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r ) )

per cases ( not o9 is_a_prefix_of f or ex t1 being Element of dom e2 st f = o9 ^ t1 ) by A26, Th10;

suppose A27: not o9 is_a_prefix_of f ; :: thesis: ( ( not <*k*> is_a_prefix_of f & (x -tree q) . f = e1 . f ) or ex r being FinSequence of NAT st
( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r ) )

A28: (x -tree q) . f = e1 . f

proof

per cases ( f = {} or ex w being Nat ex u being FinSequence st
( w < len dqq & u in dqq . (w + 1) & f = <*w*> ^ u ) ) by A15, A25, A26, TREES_3:def 15;

suppose A29: f = {} ; :: thesis: (x -tree q) . f = e1 . f

hence (x -tree q) . f = x by TREES_4:def 4
.= e1 . f by A2, A29, TREES_4:def 4 ;
:: thesis: verum

end;

suppose ex w being Nat ex u being FinSequence st
( w < len dqq & u in dqq . (w + 1) & f = <*w*> ^ u ) ; :: thesis: (x -tree q) . f = e1 . f

then consider w being Nat, u being FinSequence such that
A30: w < len (doms q) and
A31: u in (doms q) . (w + 1) and
A32: f = <*w*> ^ u by A14;
reconsider u = u as FinSequence of NAT by A32, FINSEQ_1:36;
reconsider w = w as Element of NAT by ORDINAL1:def 12;
reconsider ww = <*w*> as FinSequence of NAT ;
A33: w + 1 <> k + 1 by A27, A32, TREES_1:1;
A34: ex pp being DTree-yielding FinSequence st
( p = pp & dom (x -tree p) = tree (doms pp) ) by TREES_4:def 4;
A35: w < len q by A30, TREES_3:38;
then A36: (x -tree q) | <*w*> = q . (w + 1) by TREES_4:def 4;
( 1 <= w + 1 & w + 1 <= len p ) by A8, A35, NAT_1:11, NAT_1:13;
then A37: w + 1 in dom p by FINSEQ_3:25;
then reconsider pw1 = p . (w + 1) as DecoratedTree by TREES_3:24;
A38: q . (w + 1) = IFEQ ((w + 1),(k + 1),e2,(p . (w + 1))) by A9, A10, A17, A37
.= p . (w + 1) by A33, FUNCOP_1:def 8 ;
w + 1 in dom (doms p) by A37, TREES_3:37;
then A39: (dom (x -tree p)) | <*w*> = (doms p) . (w + 1) by A34, Th11
.= dom pw1 by A37, FUNCT_6:22
.= (doms q) . (w + 1) by A11, A37, A38, FUNCT_6:22 ;
w + 1 in dom (doms q) by A11, A37, TREES_3:37;
then (dom (x -tree q)) | <*w*> = (doms q) . (w + 1) by A14, A15, Th11;
hence (x -tree q) . f = ((x -tree q) | ww) . u by A31, A32, TREES_2:def 10
.= ((x -tree p) | ww) . u by A8, A35, A36, A38, TREES_4:def 4
.= e1 . f by A2, A31, A32, A39, TREES_2:def 10 ;
:: thesis: verum

end;

end;

end;

assume ( <*k*> is_a_prefix_of f or (x -tree q) . f <> e1 . f ) ; :: thesis: ex r being FinSequence of NAT st
( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r )
hence ex r being FinSequence of NAT st
( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r ) by A27, A28; :: thesis: verum

end;

suppose ex t1 being Element of dom e2 st f = o9 ^ t1 ; :: thesis: ( ( not <*k*> is_a_prefix_of f & (x -tree q) . f = e1 . f ) or ex r being FinSequence of NAT st
( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r ) )

then consider r being Element of dom e2 such that
A40: f = <*k*> ^ r ;
assume ( <*k*> is_a_prefix_of f or (x -tree q) . f <> e1 . f ) ; :: thesis: ex r being FinSequence of NAT st
( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r )
A41: (x -tree q) | <*k*> = q . (k + 1) by A8, A3, A22, TREES_4:def 4;
reconsider r = r as FinSequence of NAT ;
take r ; :: thesis: ( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r )
thus A42: r in dom e2 ; :: thesis: ( f = <*k*> ^ r & (x -tree q) . f = e2 . r )
thus f = <*k*> ^ r by A40; :: thesis: (x -tree q) . f = e2 . r
r in (dom (x -tree q)) | <*k*> by A1, A25, A42, TREES_1:33;
hence (x -tree q) . f = e2 . r by A24, A40, A41, TREES_2:def 10; :: thesis: verum

end;

end;

end;

hence e1 with-replacement (<*k*>,e2) = x -tree q by A1, A25, TREES_2:def 11; :: thesis: ( len q = len p & q . (k + 1) = e2 & ( for i being Nat st i in dom p & i <> k + 1 holds
q . i = p . i ) )
thus len q = len p by A8; :: thesis: ( q . (k + 1) = e2 & ( for i being Nat st i in dom p & i <> k + 1 holds
q . i = p . i ) )
thus q . (k + 1) = e2 by A24; :: thesis: for i being Nat st i in dom p & i <> k + 1 holds
q . i = p . i
let i be Nat; :: thesis: ( i in dom p & i <> k + 1 implies q . i = p . i )
assume i in dom p ; :: thesis: ( not i <> k + 1 or q . i = p . i )
then q . i = IFEQ (i,(k + 1),e2,(p . i)) by A9, A10, A17;
hence ( not i <> k + 1 or q . i = p . i ) by FUNCOP_1:def 8; :: thesis: verum