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 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 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 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 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 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 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 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 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:38;
A4: len (doms p2) = len p2 by TREES_3:38;
A5: len p = len p2 by A1, FINSEQ_3:29;
then A6: dom (doms p) = dom (doms p2) 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 p2) . i

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

end;

then A11: doms p = doms p2 by A6, A7, FINSEQ_1:13;
dom (([d1,d2] -tree p) `2) = dom ([d1,d2] -tree p) by Th24
.= tree (doms p) by Th10 ;
hence dom (([d1,d2] -tree p) `2) = dom (d2 -tree p2) by A11, 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;
A12: (([d1,d2] -tree p) `2) . x = (([d1,d2] -tree p) . a) `2 by TREES_3:39;

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

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

then ( ([d1,d2] -tree p) . x = [d1,d2] & (d2 -tree p2) . x = d2 ) by Def4;
hence (([d1,d2] -tree p) `2) . x = (d2 -tree p2) . x by A12; :: thesis: verum

end;

suppose x <> {} ; :: thesis: (([d1,d2] -tree p) `2) . x = (d2 -tree p2) . 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 `2) by Th24;
A16: p2 . (n + 1) = T `2 by A2, A13, A14, Lm2;
A17: ([d1,d2] -tree p) . a = T . q by A13, A14, A15, Th12;
(d2 -tree p2) . a = (T `2) . q by A5, A13, A15, A16, Th12;
hence (([d1,d2] -tree p) `2) . x = (d2 -tree p2) . x by A12, A17, TREES_3:39; :: thesis: verum

end;

end;