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 ;
then A6: dom (doms p) = dom (doms p2) by ;
A7: dom (doms p) = dom p by ;
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 ;
(doms p2) . i = dom (T `2) by ;
hence (doms p) . i = (doms p2) . i by ; :: thesis: verum
end;
then A11: doms p = doms p2 by ;
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 ; :: 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 ;
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 ;
(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 ; :: thesis: verum
end;
end;