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 F2 being non empty DTree-set of D2
for p being FinSequence of F
for p2 being FinSequence of F2 st dom p2 = dom p & ( for i being Element of NAT st i in dom p holds
for T being DecoratedTree of D1,D2 st T = p . i holds
p2 . i = T `2 ) holds
([d1,d2] -tree p) `2 = d2 -tree p2
let d1 be Element of D1; :: thesis: for d2 being Element of D2
for F being non empty DTree-set of D1,D2
for F2 being non empty DTree-set of D2
for p being FinSequence of F
for p2 being FinSequence of F2 st dom p2 = dom p & ( for i being Element of NAT st i in dom p holds
for T being DecoratedTree of D1,D2 st T = p . i holds
p2 . i = T `2 ) holds
([d1,d2] -tree p) `2 = d2 -tree p2
let d2 be Element of D2; :: thesis: for F being non empty DTree-set of D1,D2
for F2 being non empty DTree-set of D2
for p being FinSequence of F
for p2 being FinSequence of F2 st dom p2 = dom p & ( for i being Element of NAT st i in dom p holds
for T being DecoratedTree of D1,D2 st T = p . i holds
p2 . i = T `2 ) holds
([d1,d2] -tree p) `2 = d2 -tree p2
let F be non empty DTree-set of D1,D2; :: thesis: for F2 being non empty DTree-set of D2
for p being FinSequence of F
for p2 being FinSequence of F2 st dom p2 = dom p & ( for i being Element of NAT st i in dom p holds
for T being DecoratedTree of D1,D2 st T = p . i holds
p2 . i = T `2 ) holds
([d1,d2] -tree p) `2 = d2 -tree p2
let F2 be non empty DTree-set of D2; :: thesis: for p being FinSequence of F
for p2 being FinSequence of F2 st dom p2 = dom p & ( for i being Element of NAT st i in dom p holds
for T being DecoratedTree of D1,D2 st T = p . i holds
p2 . i = T `2 ) holds
([d1,d2] -tree p) `2 = d2 -tree p2
let p be FinSequence of F; :: thesis: for p2 being FinSequence of F2 st dom p2 = dom p & ( for i being Element of NAT st i in dom p holds
for T being DecoratedTree of D1,D2 st T = p . i holds
p2 . i = T `2 ) holds
([d1,d2] -tree p) `2 = d2 -tree p2
let p2 be FinSequence of F2; :: thesis: ( dom p2 = dom p & ( for i being Element of NAT st i in dom p holds
for T being DecoratedTree of D1,D2 st T = p . i holds
p2 . i = T `2 ) implies ([d1,d2] -tree p) `2 = d2 -tree p2 )
assume that
A1: dom p2 = dom p and
A2: for i being Element of NAT st i in dom p holds
for T being DecoratedTree of D1,D2 st T = p . i holds
p2 . i = T `2 ; :: thesis: ([d1,d2] -tree p) `2 = d2 -tree p2
set W = [d1,d2] -tree p;
set W2 = d2 -tree p2;
A3: len (doms p) = len p by TREES_3:40;
A4: len (doms p2) = len p2 by TREES_3:40;
A5: len p = len p2 by A1, FINSEQ_3:31;
A6: dom (doms p) = dom (doms p2) by A3, A4, A5, FINSEQ_3:31;
A7: dom (doms p) = dom p by A3, FINSEQ_3:31;

A8: now

let i be Nat; :: thesis: ( i in dom p implies (doms p) . i = (doms p2) . i )
assume A9: i in dom p ; :: thesis: (doms p) . i = (doms p2) . i
reconsider T = p . i as Element of F by A9, Lm1;
A10: p2 . i = T `2 by A2, A9;
A11: (doms p) . i = dom T by A9, FUNCT_6:31;
A12: (doms p2) . i = dom (T `2 ) by A1, A9, A10, FUNCT_6:31;
thus (doms p) . i = (doms p2) . i by A11, A12, Th24; :: thesis: verum

end;

A13: doms p = doms p2 by A6, A7, A8, FINSEQ_1:17;
A14: dom (([d1,d2] -tree p) `2 ) = dom ([d1,d2] -tree p) by Th24
.= tree (doms p) by Th10 ;
thus dom (([d1,d2] -tree p) `2 ) = dom (d2 -tree p2) by A13, A14, Th10; :: according to TREES_4:def 1 :: thesis: for p being Node of (([d1,d2] -tree p) `2 ) holds (([d1,d2] -tree p) `2 ) . p = (d2 -tree p2) . p
let x be Node of (([d1,d2] -tree p) `2 ); :: thesis: (([d1,d2] -tree p) `2 ) . x = (d2 -tree p2) . x
reconsider a = x as Node of ([d1,d2] -tree p) by Th24;
A15: (([d1,d2] -tree p) `2 ) . x = (([d1,d2] -tree p) . a) `2 by TREES_3:41;

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

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

A17: ( ([d1,d2] -tree p) . x = [d1,d2] & (d2 -tree p2) . x = d2 ) by A16, Def4;
thus (([d1,d2] -tree p) `2 ) . x = (d2 -tree p2) . x by A15, A17, MCART_1:7; :: thesis: verum

end;

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

consider n being Element of NAT , T being DecoratedTree, q being Node of T such that
A19: n < len p and
A20: T = p . (n + 1) and
A21: a = <*n*> ^ q by A18, Th11;
reconsider T = T as Element of F by A19, A20, Lm3;
reconsider q = q as Node of (T `2 ) by Th24;
A22: p2 . (n + 1) = T `2 by A2, A19, A20, Lm2;
A23: ([d1,d2] -tree p) . a = T . q by A19, A20, A21, Th12;
A24: (d2 -tree p2) . a = (T `2 ) . q by A5, A19, A21, A22, Th12;
thus (([d1,d2] -tree p) `2 ) . x = (d2 -tree p2) . x by A15, A23, A24, TREES_3:41; :: thesis: verum

end;

end;