let b be object ; :: thesis: for c being set
for d being DecoratedTree
for p, q being non empty DTree-yielding FinSequence st dom q = dom p & ( for i being Nat
for d1 being DecoratedTree st i in dom p & d1 = p . i holds
q . i = (d1,c) <- d ) holds
((b -tree p),c) <- d = b -tree q
let c be set ; :: thesis: for d being DecoratedTree
for p, q being non empty DTree-yielding FinSequence st dom q = dom p & ( for i being Nat
for d1 being DecoratedTree st i in dom p & d1 = p . i holds
q . i = (d1,c) <- d ) holds
((b -tree p),c) <- d = b -tree q
let d be DecoratedTree; :: thesis: for p, q being non empty DTree-yielding FinSequence st dom q = dom p & ( for i being Nat
for d1 being DecoratedTree st i in dom p & d1 = p . i holds
q . i = (d1,c) <- d ) holds
((b -tree p),c) <- d = b -tree q
let p, q be non empty DTree-yielding FinSequence; :: thesis: ( dom q = dom p & ( for i being Nat
for d1 being DecoratedTree st i in dom p & d1 = p . i holds
q . i = (d1,c) <- d ) implies ((b -tree p),c) <- d = b -tree q )
assume that
A1: dom q = dom p and
A2: for i being Nat
for d1 being DecoratedTree st i in dom p & d1 = p . i holds
q . i = (d1,c) <- d ; :: thesis: ((b -tree p),c) <- d = b -tree q
A3: ( dom (b -tree p) = tree (doms p) & dom (b -tree q) = tree (doms q) ) by TREES_4:10;
A4: Leaves (tree (doms p)) = { (<*i*> ^ q) where i is Nat, q is FinSequence of NAT , d is Tree : ( q in Leaves d & i + 1 in dom (doms p) & d = (doms p) . (i + 1) ) } by ThL0;
A5: ( dom (doms p) = dom p & dom (doms q) = dom q ) by FUNCT_6:def 2;
then A6: ( len (doms p) = len p & len p = len q & len q = len (doms q) ) by A1, FINSEQ_3:29;
AA: dom (((b -tree p),c) <- d) = dom (b -tree q)

proof

let x be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not x in dom (((b -tree p),c) <- d) or x in dom (b -tree q) ) & ( not x in dom (b -tree q) or x in dom (((b -tree p),c) <- d) ) )

hereby :: thesis: ( not x in dom (b -tree q) or x in dom (((b -tree p),c) <- d) )

assume x in dom (((b -tree p),c) <- d) ; :: thesis: x in dom (b -tree q)
then reconsider r = x as Node of (((b -tree p),c) <- d) ;

per cases ( r in dom (b -tree p) or ex q being Node of (b -tree p) ex s being Node of d st
( q in Leaves (dom (b -tree p)) & (b -tree p) . q = c & r = q ^ s ) ) by TREES_4:def 7;

suppose r in dom (b -tree p) ; :: thesis: x in dom (b -tree q)

per cases then ( r = {} or ex n being Nat ex q being FinSequence st
( n < len (doms p) & q in (doms p) . (n + 1) & x = <*n*> ^ q ) ) by A3, TREES_3:def 15;

suppose r = {} ; :: thesis: x in dom (b -tree q)

hence x in dom (b -tree q) by TREES_1:22; :: thesis: verum

end;

suppose ex n being Nat ex q being FinSequence st
( n < len (doms p) & q in (doms p) . (n + 1) & x = <*n*> ^ q ) ; :: thesis: x in dom (b -tree q)

then consider n being Nat, w being FinSequence such that
A7: ( n < len (doms p) & w in (doms p) . (n + 1) & x = <*n*> ^ w ) ;
A9: ( 1 <= n + 1 & n + 1 <= len (doms p) ) by A7, NAT_1:11, NAT_1:13;
reconsider pn = p . (n + 1) as DecoratedTree by A5, A9, FINSEQ_3:25, TREES_3:24;
reconsider qn = q . (n + 1) as DecoratedTree by A1, A9, A5, FINSEQ_3:25, TREES_3:24;
qn = (pn,c) <- d by A2, A5, A9, FINSEQ_3:25;
then ( (doms p) . (n + 1) = dom pn & dom pn c= dom qn & dom qn = (doms q) . (n + 1) ) by A1, A5, A9, TREES_4:def 7, FINSEQ_3:25, FUNCT_6:def 2;
hence x in dom (b -tree q) by A3, A6, A7, TREES_3:def 15; :: thesis: verum

end;

end;

end;

suppose ex q being Node of (b -tree p) ex s being Node of d st
( q in Leaves (dom (b -tree p)) & (b -tree p) . q = c & r = q ^ s ) ; :: thesis: x in dom (b -tree q)

then consider w being Node of (b -tree p), s being Node of d such that
A8: ( w in Leaves (dom (b -tree p)) & (b -tree p) . w = c & r = w ^ s ) ;
consider i being Nat, u being FinSequence of NAT , d2 being Tree such that
A9: ( w = <*i*> ^ u & u in Leaves d2 & i + 1 in dom (doms p) & d2 = (doms p) . (i + 1) ) by A8, A3, A4;
reconsider p1 = p . (i + 1) as DecoratedTree by A5, A9, TREES_3:24;
B1: w ^ s = <*i*> ^ (u ^ s) by A9, FINSEQ_1:32;
B2: q . (i + 1) = (p1,c) <- d by A2, A5, A9;
B3: dom p1 = d2 by A5, A9, FUNCT_6:def 2;
reconsider u = u as Node of p1 by A5, A9, FUNCT_6:def 2;
B6: i + 1 <= len (doms p) by A9, FINSEQ_3:25;
then B4: i < len (doms p) by NAT_1:13;
p1 . u = c by B6, A6, A8, A9, NAT_1:13, TREES_4:12;
then B5: ( u ^ s in dom ((p1,c) <- d) & dom ((p1,c) <- d) = (doms q) . (i + 1) ) by B3, A1, A5, A9, B2, TREES_4:def 7, FUNCT_6:def 2;
thus x in dom (b -tree q) by B1, B4, B5, A3, A6, A8, TREES_3:def 15; :: thesis: verum

end;

end;

end;

assume x in dom (b -tree q) ; :: thesis: x in dom (((b -tree p),c) <- d)
then reconsider r = x as Node of (b -tree q) ;

per cases ( r = {} or ex i being Nat ex w being FinSequence st
( i < len (doms q) & w in (doms q) . (i + 1) & x = <*i*> ^ w ) ) by A3, TREES_3:def 15;

suppose r = {} ; :: thesis: x in dom (((b -tree p),c) <- d)

hence x in dom (((b -tree p),c) <- d) by TREES_1:22; :: thesis: verum

end;

suppose ex i being Nat ex w being FinSequence st
( i < len (doms q) & w in (doms q) . (i + 1) & x = <*i*> ^ w ) ; :: thesis: x in dom (((b -tree p),c) <- d)

then consider n being Nat, w being FinSequence such that
C1: ( n < len (doms q) & w in (doms q) . (n + 1) & x = <*n*> ^ w ) ;
C4: ( 1 <= n + 1 & n + 1 <= len (doms q) ) by C1, NAT_1:11, NAT_1:13;
then C2: n + 1 in dom (doms q) by FINSEQ_3:25;
reconsider qi = q . (n + 1) as DecoratedTree by C4, A5, FINSEQ_3:25, TREES_3:24;
reconsider p1 = p . (n + 1) as DecoratedTree by A1, A5, C4, FINSEQ_3:25, TREES_3:24;
C3: ( dom qi = (doms q) . (n + 1) & dom p1 = (doms p) . (n + 1) ) by A1, A5, C4, FINSEQ_3:25, FUNCT_6:def 2;
qi = (p1,c) <- d by C4, A1, A2, A5, FINSEQ_3:25;

per cases then ( w in dom p1 or ex u being Node of p1 ex s being Node of d st
( u in Leaves (dom p1) & p1 . u = c & w = u ^ s ) ) by C1, C3, TREES_4:def 7;

suppose w in dom p1 ; :: thesis: x in dom (((b -tree p),c) <- d)

then ( x in dom (b -tree p) & dom (b -tree p) c= dom (((b -tree p),c) <- d) ) by A3, A6, C1, C3, TREES_4:def 7, TREES_3:def 15;
hence x in dom (((b -tree p),c) <- d) ; :: thesis: verum

end;

suppose ex u being Node of p1 ex s being Node of d st
( u in Leaves (dom p1) & p1 . u = c & w = u ^ s ) ; :: thesis: x in dom (((b -tree p),c) <- d)

then consider u being Node of p1, s being Node of d such that
C4: ( u in Leaves (dom p1) & p1 . u = c & w = u ^ s ) ;
C5: <*n*> ^ u in Leaves (tree (doms p)) by A4, C4, A5, A1, C2, C3;
(b -tree p) . (<*n*> ^ u) = c by C1, A6, C4, TREES_4:12;
then (<*n*> ^ u) ^ s in dom (((b -tree p),c) <- d) by A3, C5, TREES_4:def 7;
hence x in dom (((b -tree p),c) <- d) by C1, C4, FINSEQ_1:32; :: thesis: verum

end;

end;

end;

end;

end;

now :: thesis: for x being object st x in dom (b -tree q) holds
(((b -tree p),c) <- d) . x = (b -tree q) . x

let x be object ; :: thesis: ( x in dom (b -tree q) implies (((b -tree p),c) <- d) . b₁ = (b -tree q) . b₁ )
assume x in dom (b -tree q) ; :: thesis: (((b -tree p),c) <- d) . b₁ = (b -tree q) . b₁
then reconsider r = x as Node of (b -tree q) ;

per cases ( r = {} or ex i being Nat ex w being FinSequence st
( i < len (doms q) & w in (doms q) . (i + 1) & x = <*i*> ^ w ) ) by A3, TREES_3:def 15;

suppose C1: r = {} ; :: thesis: (((b -tree p),c) <- d) . b₁ = (b -tree q) . b₁

reconsider r = {} as Node of (b -tree p) by TREES_1:22;
for i being Nat
for q being FinSequence of NAT
for d being Tree holds
( not r = <*i*> ^ q or not q in Leaves d or not i + 1 in dom (doms p) or not d = (doms p) . (i + 1) ) ;
then r nin Leaves (dom (b -tree p)) by A4, A3;
hence (((b -tree p),c) <- d) . x = (b -tree p) . r by C1, TREES_4:def 7
.= b by TREES_4:def 4
.= (b -tree q) . x by C1, TREES_4:def 4 ;
:: thesis: verum

end;

suppose ex i being Nat ex w being FinSequence st
( i < len (doms q) & w in (doms q) . (i + 1) & x = <*i*> ^ w ) ; :: thesis: (((b -tree p),c) <- d) . b₁ = (b -tree q) . b₁

then consider n being Nat, w being FinSequence such that
C1: ( n < len (doms q) & w in (doms q) . (n + 1) & x = <*n*> ^ w ) ;
C5: ( 1 <= n + 1 & n + 1 <= len (doms q) ) by C1, NAT_1:11, NAT_1:13;
then C2: n + 1 in dom (doms q) by FINSEQ_3:25;
reconsider qi = q . (n + 1) as DecoratedTree by C5, A5, FINSEQ_3:25, TREES_3:24;
reconsider p1 = p . (n + 1) as DecoratedTree by A1, A5, C5, FINSEQ_3:25, TREES_3:24;
C3: ( dom qi = (doms q) . (n + 1) & dom p1 = (doms p) . (n + 1) ) by A1, A5, C5, FINSEQ_3:25, FUNCT_6:def 2;
C4: qi = (p1,c) <- d by C5, A1, A2, A5, FINSEQ_3:25;

per cases then ( ( w in dom p1 & w nin Leaves (dom p1) ) or ( w in dom p1 & p1 . w <> c ) or ( w in dom p1 & w in Leaves (dom p1) & p1 . w = c ) or ex u being Node of p1 ex s being Node of d st
( u in Leaves (dom p1) & p1 . u = c & w = u ^ s ) ) by C1, C3, TREES_4:def 7;

suppose D1: ( w in dom p1 & w nin Leaves (dom p1) ) ; :: thesis: (((b -tree p),c) <- d) . b₁ = (b -tree q) . b₁

D4: ( qi . w = p1 . w & dom p1 c= dom qi ) by D1, C4, TREES_4:def 7;
D5: x is Node of (b -tree p) by C1, A6, A3, C3, D1, TREES_3:def 15;

now :: thesis: for i being Nat
for q being FinSequence of NAT
for d being Tree holds
( not r = <*i*> ^ q or not q in Leaves d or not i + 1 in dom (doms p) or not d = (doms p) . (i + 1) )

given i being Nat, q being FinSequence of NAT , d being Tree such that D2: ( r = <*i*> ^ q & q in Leaves d & i + 1 in dom (doms p) & d = (doms p) . (i + 1) ) ; :: thesis: contradiction
( i = r . 1 & r . 1 = n & q = w ) by C1, D2, FINSEQ_1:41, HILBERT2:2;
hence contradiction by D1, A5, D2, FUNCT_6:def 2; :: thesis: verum

end;

then r nin Leaves (dom (b -tree p)) by A4, A3;
hence (((b -tree p),c) <- d) . x = (b -tree p) . r by D5, TREES_4:def 7
.= p1 . w by C1, A6, D1, TREES_4:12
.= (b -tree q) . x by C1, A6, D1, D4, TREES_4:12 ;
:: thesis: verum

end;

suppose D1: ( w in dom p1 & p1 . w <> c ) ; :: thesis: (((b -tree p),c) <- d) . b₁ = (b -tree q) . b₁

D4: ( qi . w = p1 . w & dom p1 c= dom qi ) by D1, C4, TREES_4:def 7;
D5: x is Node of (b -tree p) by C1, A6, A3, C3, D1, TREES_3:def 15;
(b -tree p) . r <> c by C1, A6, D1, TREES_4:12;
hence (((b -tree p),c) <- d) . x = (b -tree p) . r by D5, TREES_4:def 7
.= p1 . w by C1, A6, D1, TREES_4:12
.= (b -tree q) . x by C1, A6, D1, D4, TREES_4:12 ;
:: thesis: verum

end;

suppose C7: ( w in dom p1 & w in Leaves (dom p1) & p1 . w = c ) ; :: thesis: (((b -tree p),c) <- d) . b₁ = (b -tree q) . b₁

then reconsider u = w as Node of p1 ;
reconsider s = {} as Node of d by TREES_1:22;
C71: w = u ^ s ;
C5: <*n*> ^ u in Leaves (tree (doms p)) by A4, C7, A5, A1, C2, C3;
C6: (b -tree p) . (<*n*> ^ u) = c by C1, A6, C7, TREES_4:12;
(((b -tree p),c) <- d) . ((<*n*> ^ u) ^ s) = d . s by A3, C5, C6, TREES_4:def 7
.= qi . w by C4, C7, C71, TREES_4:def 7
.= (b -tree q) . x by C1, A6, C3, TREES_4:12 ;
hence (((b -tree p),c) <- d) . x = (b -tree q) . x by C1; :: thesis: verum

end;

suppose ex u being Node of p1 ex s being Node of d st
( u in Leaves (dom p1) & p1 . u = c & w = u ^ s ) ; :: thesis: (((b -tree p),c) <- d) . b₁ = (b -tree q) . b₁

then consider u being Node of p1, s being Node of d such that
C7: ( u in Leaves (dom p1) & p1 . u = c & w = u ^ s ) ;
C5: <*n*> ^ u in Leaves (tree (doms p)) by A4, C7, A5, A1, C2, C3;
C6: (b -tree p) . (<*n*> ^ u) = c by C1, A6, C7, TREES_4:12;
(((b -tree p),c) <- d) . ((<*n*> ^ u) ^ s) = d . s by A3, C5, C6, TREES_4:def 7
.= qi . w by C4, C7, TREES_4:def 7
.= (b -tree q) . x by C1, A6, C3, TREES_4:12 ;
hence (((b -tree p),c) <- d) . x = (b -tree q) . x by C1, C7, FINSEQ_1:32; :: thesis: verum

end;

end;

end;

end;

end;

hence ((b -tree p),c) <- d = b -tree q by AA, FUNCT_1:2; :: thesis: verum