let D1, D2 be non empty set ; :: thesis: for d1 being Element of D1

for d2 being Element of D2

for F being non empty DTree-set of D1,D2

for F1 being non empty DTree-set of D1

for p being FinSequence of F

for p1 being FinSequence of F1 st dom p1 = dom p & ( for i being Nat st i in dom p holds

for T being DecoratedTree of D1,D2 st T = p . i holds

p1 . i = T `1 ) holds

([d1,d2] -tree p) `1 = d1 -tree p1

let d1 be Element of D1; :: thesis: for d2 being Element of D2

for F being non empty DTree-set of D1,D2

for F1 being non empty DTree-set of D1

for p being FinSequence of F

for p1 being FinSequence of F1 st dom p1 = dom p & ( for i being Nat st i in dom p holds

for T being DecoratedTree of D1,D2 st T = p . i holds

p1 . i = T `1 ) holds

([d1,d2] -tree p) `1 = d1 -tree p1

let d2 be Element of D2; :: thesis: for F being non empty DTree-set of D1,D2

for F1 being non empty DTree-set of D1

for p being FinSequence of F

for p1 being FinSequence of F1 st dom p1 = dom p & ( for i being Nat st i in dom p holds

for T being DecoratedTree of D1,D2 st T = p . i holds

p1 . i = T `1 ) holds

([d1,d2] -tree p) `1 = d1 -tree p1

let F be non empty DTree-set of D1,D2; :: thesis: for F1 being non empty DTree-set of D1

for p being FinSequence of F

for p1 being FinSequence of F1 st dom p1 = dom p & ( for i being Nat st i in dom p holds

for T being DecoratedTree of D1,D2 st T = p . i holds

p1 . i = T `1 ) holds

([d1,d2] -tree p) `1 = d1 -tree p1

let F1 be non empty DTree-set of D1; :: thesis: for p being FinSequence of F

for p1 being FinSequence of F1 st dom p1 = dom p & ( for i being Nat st i in dom p holds

for T being DecoratedTree of D1,D2 st T = p . i holds

p1 . i = T `1 ) holds

([d1,d2] -tree p) `1 = d1 -tree p1

let p be FinSequence of F; :: thesis: for p1 being FinSequence of F1 st dom p1 = dom p & ( for i being Nat st i in dom p holds

for T being DecoratedTree of D1,D2 st T = p . i holds

p1 . i = T `1 ) holds

([d1,d2] -tree p) `1 = d1 -tree p1

let p1 be FinSequence of F1; :: thesis: ( dom p1 = dom p & ( for i being Nat st i in dom p holds

for T being DecoratedTree of D1,D2 st T = p . i holds

p1 . i = T `1 ) implies ([d1,d2] -tree p) `1 = d1 -tree p1 )

assume that

A1: dom p1 = dom p and

A2: for i being Nat st i in dom p holds

for T being DecoratedTree of D1,D2 st T = p . i holds

p1 . i = T `1 ; :: thesis: ([d1,d2] -tree p) `1 = d1 -tree p1

set W = [d1,d2] -tree p;

set W1 = d1 -tree p1;

A3: len (doms p) = len p by TREES_3:38;

A4: len (doms p1) = len p1 by TREES_3:38;

A5: len p = len p1 by A1, FINSEQ_3:29;

then A6: dom (doms p) = dom (doms p1) by A3, A4, FINSEQ_3:29;

A7: dom (doms p) = dom p by A3, FINSEQ_3:29;

dom (([d1,d2] -tree p) `1) = dom ([d1,d2] -tree p) by Th24

.= tree (doms p) by Th10 ;

hence dom (([d1,d2] -tree p) `1) = dom (d1 -tree p1) by A11, Th10; :: according to TREES_4:def 1 :: thesis: for p being Node of (([d1,d2] -tree p) `1) holds (([d1,d2] -tree p) `1) . p = (d1 -tree p1) . p

let x be Node of (([d1,d2] -tree p) `1); :: thesis: (([d1,d2] -tree p) `1) . x = (d1 -tree p1) . x

reconsider a = x as Node of ([d1,d2] -tree p) by Th24;

A12: (([d1,d2] -tree p) `1) . x = (([d1,d2] -tree p) . a) `1 by TREES_3:39;

for d2 being Element of D2

for F being non empty DTree-set of D1,D2

for F1 being non empty DTree-set of D1

for p being FinSequence of F

for p1 being FinSequence of F1 st dom p1 = dom p & ( for i being Nat st i in dom p holds

for T being DecoratedTree of D1,D2 st T = p . i holds

p1 . i = T `1 ) holds

([d1,d2] -tree p) `1 = d1 -tree p1

let d1 be Element of D1; :: thesis: for d2 being Element of D2

for F being non empty DTree-set of D1,D2

for F1 being non empty DTree-set of D1

for p being FinSequence of F

for p1 being FinSequence of F1 st dom p1 = dom p & ( for i being Nat st i in dom p holds

for T being DecoratedTree of D1,D2 st T = p . i holds

p1 . i = T `1 ) holds

([d1,d2] -tree p) `1 = d1 -tree p1

let d2 be Element of D2; :: thesis: for F being non empty DTree-set of D1,D2

for F1 being non empty DTree-set of D1

for p being FinSequence of F

for p1 being FinSequence of F1 st dom p1 = dom p & ( for i being Nat st i in dom p holds

for T being DecoratedTree of D1,D2 st T = p . i holds

p1 . i = T `1 ) holds

([d1,d2] -tree p) `1 = d1 -tree p1

let F be non empty DTree-set of D1,D2; :: thesis: for F1 being non empty DTree-set of D1

for p being FinSequence of F

for p1 being FinSequence of F1 st dom p1 = dom p & ( for i being Nat st i in dom p holds

for T being DecoratedTree of D1,D2 st T = p . i holds

p1 . i = T `1 ) holds

([d1,d2] -tree p) `1 = d1 -tree p1

let F1 be non empty DTree-set of D1; :: thesis: for p being FinSequence of F

for p1 being FinSequence of F1 st dom p1 = dom p & ( for i being Nat st i in dom p holds

for T being DecoratedTree of D1,D2 st T = p . i holds

p1 . i = T `1 ) holds

([d1,d2] -tree p) `1 = d1 -tree p1

let p be FinSequence of F; :: thesis: for p1 being FinSequence of F1 st dom p1 = dom p & ( for i being Nat st i in dom p holds

for T being DecoratedTree of D1,D2 st T = p . i holds

p1 . i = T `1 ) holds

([d1,d2] -tree p) `1 = d1 -tree p1

let p1 be FinSequence of F1; :: thesis: ( dom p1 = dom p & ( for i being Nat st i in dom p holds

for T being DecoratedTree of D1,D2 st T = p . i holds

p1 . i = T `1 ) implies ([d1,d2] -tree p) `1 = d1 -tree p1 )

assume that

A1: dom p1 = dom p and

A2: for i being Nat st i in dom p holds

for T being DecoratedTree of D1,D2 st T = p . i holds

p1 . i = T `1 ; :: thesis: ([d1,d2] -tree p) `1 = d1 -tree p1

set W = [d1,d2] -tree p;

set W1 = d1 -tree p1;

A3: len (doms p) = len p by TREES_3:38;

A4: len (doms p1) = len p1 by TREES_3:38;

A5: len p = len p1 by A1, FINSEQ_3:29;

then A6: dom (doms p) = dom (doms p1) by A3, A4, FINSEQ_3:29;

A7: dom (doms p) = dom p by A3, FINSEQ_3:29;

now :: thesis: for i being Nat st i in dom p holds

(doms p) . i = (doms p1) . i

then A11:
doms p = doms p1
by A6, A7, FINSEQ_1:13;(doms p) . i = (doms p1) . i

let i be Nat; :: thesis: ( i in dom p implies (doms p) . i = (doms p1) . i )

assume A8: i in dom p ; :: thesis: (doms p) . i = (doms p1) . i

then reconsider T = p . i as Element of F by Lm1;

A9: p1 . i = T `1 by A2, A8;

A10: (doms p) . i = dom T by A8, FUNCT_6:22;

(doms p1) . i = dom (T `1) by A1, A8, A9, FUNCT_6:22;

hence (doms p) . i = (doms p1) . i by A10, Th24; :: thesis: verum

end;assume A8: i in dom p ; :: thesis: (doms p) . i = (doms p1) . i

then reconsider T = p . i as Element of F by Lm1;

A9: p1 . i = T `1 by A2, A8;

A10: (doms p) . i = dom T by A8, FUNCT_6:22;

(doms p1) . i = dom (T `1) by A1, A8, A9, FUNCT_6:22;

hence (doms p) . i = (doms p1) . i by A10, Th24; :: thesis: verum

dom (([d1,d2] -tree p) `1) = dom ([d1,d2] -tree p) by Th24

.= tree (doms p) by Th10 ;

hence dom (([d1,d2] -tree p) `1) = dom (d1 -tree p1) by A11, Th10; :: according to TREES_4:def 1 :: thesis: for p being Node of (([d1,d2] -tree p) `1) holds (([d1,d2] -tree p) `1) . p = (d1 -tree p1) . p

let x be Node of (([d1,d2] -tree p) `1); :: thesis: (([d1,d2] -tree p) `1) . x = (d1 -tree p1) . x

reconsider a = x as Node of ([d1,d2] -tree p) by Th24;

A12: (([d1,d2] -tree p) `1) . x = (([d1,d2] -tree p) . a) `1 by TREES_3:39;

per cases
( x = {} or x <> {} )
;

end;

suppose
x = {}
; :: thesis: (([d1,d2] -tree p) `1) . x = (d1 -tree p1) . x

then
( ([d1,d2] -tree p) . x = [d1,d2] & (d1 -tree p1) . x = d1 )
by Def4;

hence (([d1,d2] -tree p) `1) . x = (d1 -tree p1) . x by A12; :: thesis: verum

end;hence (([d1,d2] -tree p) `1) . x = (d1 -tree p1) . x by A12; :: thesis: verum

suppose
x <> {}
; :: thesis: (([d1,d2] -tree p) `1) . x = (d1 -tree p1) . x

then consider n being Nat, T being DecoratedTree, q being Node of T such that

A13: n < len p and

A14: T = p . (n + 1) and

A15: a = <*n*> ^ q by Th11;

reconsider T = T as Element of F by A13, A14, Lm3;

reconsider q = q as Node of (T `1) by Th24;

A16: p1 . (n + 1) = T `1 by A2, A13, A14, Lm2;

A17: ([d1,d2] -tree p) . a = T . q by A13, A14, A15, Th12;

(d1 -tree p1) . a = (T `1) . q by A5, A13, A15, A16, Th12;

hence (([d1,d2] -tree p) `1) . x = (d1 -tree p1) . x by A12, A17, TREES_3:39; :: thesis: verum

end;A13: n < len p and

A14: T = p . (n + 1) and

A15: a = <*n*> ^ q by Th11;

reconsider T = T as Element of F by A13, A14, Lm3;

reconsider q = q as Node of (T `1) by Th24;

A16: p1 . (n + 1) = T `1 by A2, A13, A14, Lm2;

A17: ([d1,d2] -tree p) . a = T . q by A13, A14, A15, Th12;

(d1 -tree p1) . a = (T `1) . q by A5, A13, A15, A16, Th12;

hence (([d1,d2] -tree p) `1) . x = (d1 -tree p1) . x by A12, A17, TREES_3:39; :: thesis: verum