let e1, e2 be finite DecoratedTree; :: thesis:
let x be set ; :: thesis:
let k be Element of NAT ; :: thesis:
let p be DTree-yielding FinSequence; :: thesis:
assume that
A1: <*k*> in dom e1 and
A2: e1 = x -tree p ; :: thesis:
set o = <*k*>;
deffunc H₁( Nat) -> set = IFEQ $1,(k + 1),e2,(p . $1);
consider q being FinSequence such that
A3: len q = len p and
A4: for i being Nat st i in dom q holds
q . i = H₁(i) from FINSEQ_1:sch 2();
A5: dom q = Seg (len p) by A3, FINSEQ_1:def 3;
A6: dom p = Seg (len p) by FINSEQ_1:def 3;
A7: dom q = dom p by A3, FINSEQ_3:31;

now

let x be set ; :: thesis:
assume A8: x in dom q ; :: thesis:
then reconsider i = x as Element of NAT ;
A9: q . i = IFEQ i,(k + 1),e2,(p . i) by A4, A8;
( i = k + 1 or i <> k + 1 ) ;
then ( q . i = e2 or q . i = p . i ) by A9, FUNCOP_1:def 8;
hence q . x is DecoratedTree by A7, A8, TREES_3:26; :: thesis:

end;

then reconsider q = q as DTree-yielding FinSequence by TREES_3:26;
take q ; :: thesis:
consider j being Element of NAT , T being DecoratedTree, w being Node of T such that
A10: j < len p and
T = p . (j + 1) and
A11: <*k*> = <*j*> ^ w by A1, A2, TREES_4:11;
<*j*> = <*k*> by A11, TREES_1:6;
then A12: j = <*k*> . 1 by FINSEQ_1:def 8
.= k by FINSEQ_1:def 8 ;
then ( 1 <= k + 1 & k + 1 <= len p ) by A10, NAT_1:11, NAT_1:13;
then A13: k + 1 in dom p by FINSEQ_3:27;
then k + 1 in Seg (len p) by FINSEQ_1:def 3;
then A14: q . (k + 1) = IFEQ (k + 1),(k + 1),e2,(p . (k + 1)) by A4, A5
.= e2 by FUNCOP_1:def 8 ;
consider qq being DTree-yielding FinSequence such that
A15: ( q = qq & dom (x -tree q) = tree (doms qq) ) by TREES_4:def 4;
consider pp being DTree-yielding FinSequence such that
A16: ( p = pp & dom (x -tree p) = tree (doms pp) ) by TREES_4:def 4;
reconsider dqq = doms qq as Tree-yielding FinSequence ;
A17: len (doms pp) = len p by A16, TREES_3:40
.= len (doms qq) by A3, A15, TREES_3:40 ;
A18: dom (doms pp) = dom p by A16, TREES_3:39;

A19: now

let i be Element of NAT ; :: thesis:
assume A20: ( i in dom (doms pp) & i <> k + 1 ) ; :: thesis:
then A21: q . i = IFEQ i,(k + 1),e2,(p . i) by A4, A6, A18, A5
.= p . i by A20, FUNCOP_1:def 8 ;
reconsider pii = p . i as DecoratedTree by A18, A20, TREES_3:26;
thus (doms pp) . i = dom pii by A16, A18, A20, FUNCT_6:31
.= (doms qq) . i by A7, A15, A18, A20, A21, FUNCT_6:31 ; :: thesis:

end;

(doms qq) . (k + 1) = dom e2 by A7, A13, A14, A15, FUNCT_6:31;
then A22: dom (x -tree q) = (dom e1) with-replacement <*k*>,(dom e2) by A2, A13, A15, A16, A17, A18, A19, Th18;
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

let f be FinSequence of NAT ; :: thesis:
assume A23: f in (dom e1) with-replacement <*k*>,(dom e2) ; :: thesis:
reconsider o' = <*k*> as Element of dom e1 by A1;

per cases by A23, Th15;

suppose A24: not o' is_a_prefix_of f ; :: thesis:

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

proof

per cases by A15, A22, A23, TREES_3:def 15;

suppose A26: f = {} ; :: thesis:

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

end;

suppose ex w being Element of NAT ex u being FinSequence st
( w < len dqq & u in dqq . (w + 1) & f = <*w*> ^ u ) ; :: thesis:

then consider w being Element of NAT , u being FinSequence such that
A27: w < len (doms q) and
A28: u in (doms q) . (w + 1) and
A29: f = <*w*> ^ u by A15;
reconsider u = u as FinSequence of NAT by A29, FINSEQ_1:50;
reconsider ww = <*w*> as FinSequence of NAT ;
A30: w + 1 <> k + 1 by A24, A29, TREES_1:8;
A31: w < len q by A27, TREES_3:40;
then ( 1 <= w + 1 & w + 1 <= len p ) by A3, NAT_1:11, NAT_1:13;
then A32: w + 1 in dom p by FINSEQ_3:27;
A33: (x -tree q) | <*w*> = q . (w + 1) by A31, TREES_4:def 4;
A34: w + 1 in dom (doms p) by A32, TREES_3:39;
A35: w + 1 in dom (doms q) by A7, A32, TREES_3:39;
A36: q . (w + 1) = IFEQ (w + 1),(k + 1),e2,(p . (w + 1)) by A4, A6, A32, A5
.= p . (w + 1) by A30, FUNCOP_1:def 8 ;
reconsider pw1 = p . (w + 1) as DecoratedTree by A32, TREES_3:26;
A37: (dom (x -tree q)) | <*w*> = (doms q) . (w + 1) by A15, A35, Th16;
consider pp being DTree-yielding FinSequence such that
A38: ( p = pp & dom (x -tree p) = tree (doms pp) ) by TREES_4:def 4;
A39: (dom (x -tree p)) | <*w*> = (doms p) . (w + 1) by A34, A38, Th16
.= dom pw1 by A32, FUNCT_6:31
.= (doms q) . (w + 1) by A7, A32, A36, FUNCT_6:31 ;
thus (x -tree q) . f = ((x -tree q) | ww) . u by A28, A29, A37, TREES_2:def 11
.= ((x -tree p) | ww) . u by A3, A31, A33, A36, TREES_4:def 4
.= e1 . f by A2, A28, A29, A39, TREES_2:def 11 ; :: thesis:

end;

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

end;

suppose ex t1 being Element of dom e2 st f = o' ^ t1 ; :: thesis:

then consider r being Element of dom e2 such that
A40: f = <*k*> ^ r ;
reconsider r = r as FinSequence of NAT ;
assume ( <*k*> is_a_prefix_of f or (x -tree q) . f <> e1 . f ) ; :: thesis:
take r ; :: thesis:
thus A41: r in dom e2 ; :: thesis:
A42: (x -tree q) | <*k*> = q . (k + 1) by A3, A10, A12, TREES_4:def 4;
A43: r in (dom (x -tree q)) | <*k*> by A1, A22, A41, TREES_1:66;
thus f = <*k*> ^ r by A40; :: thesis:
thus (x -tree q) . f = e2 . r by A14, A40, A42, A43, TREES_2:def 11; :: thesis:

end;

hence e1 with-replacement <*k*>,e2 = x -tree q by A1, A22, TREES_2:def 12; :: thesis:
thus len q = len p by A3; :: thesis:
thus q . (k + 1) = e2 by A14; :: thesis:
let i be Element of NAT ; :: thesis:
assume i in dom p ; :: thesis:
then q . i = IFEQ i,(k + 1),e2,(p . i) by A4, A6, A5;
hence ( not i <> k + 1 or q . i = p . i ) by FUNCOP_1:def 8; :: thesis: