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 ;
then A6: dom (doms p) = dom (doms p1) by ;
A7: dom (doms p) = dom p by ;
now :: thesis: for i being Nat st i in dom p holds
(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 ;
(doms p1) . i = dom (T `1) by ;
hence (doms p) . i = (doms p1) . i by ; :: thesis: verum
end;
then A11: doms p = doms p1 by ;
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 ; :: 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 <> {} ) ;
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;
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 ;
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 ;
(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 ; :: thesis: verum
end;
end;