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 p being FinSequence of F ex p2 being FinSequence of Trees D2 st
( dom p2 = dom p & ( for i being Nat st i in dom p holds
ex T being Element of F st
( T = p . i & p2 . i = T `2 ) ) & ([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 p being FinSequence of F ex p2 being FinSequence of Trees D2 st
( dom p2 = dom p & ( for i being Nat st i in dom p holds
ex T being Element of F st
( T = p . i & p2 . i = T `2 ) ) & ([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 p being FinSequence of F ex p2 being FinSequence of Trees D2 st
( dom p2 = dom p & ( for i being Nat st i in dom p holds
ex T being Element of F st
( T = p . i & p2 . i = T `2 ) ) & ([d1,d2] -tree p) `2 = d2 -tree p2 )

let F be non empty DTree-set of D1,D2; :: thesis: for p being FinSequence of F ex p2 being FinSequence of Trees D2 st
( dom p2 = dom p & ( for i being Nat st i in dom p holds
ex T being Element of F st
( T = p . i & p2 . i = T `2 ) ) & ([d1,d2] -tree p) `2 = d2 -tree p2 )

let p be FinSequence of F; :: thesis: ex p2 being FinSequence of Trees D2 st
( dom p2 = dom p & ( for i being Nat st i in dom p holds
ex T being Element of F st
( T = p . i & p2 . i = T `2 ) ) & ([d1,d2] -tree p) `2 = d2 -tree p2 )

A1: Seg (len p) = dom p by FINSEQ_1:def 3;
defpred S1[ Nat, set ] means ex T being Element of F st
( T = p . \$1 & \$2 = T `2 );
A2: for i being Nat st i in Seg (len p) holds
ex x being Element of Trees D2 st S1[i,x]
proof
let i be Nat; :: thesis: ( i in Seg (len p) implies ex x being Element of Trees D2 st S1[i,x] )
assume i in Seg (len p) ; :: thesis: ex x being Element of Trees D2 st S1[i,x]
then reconsider T = p . i as Element of F by ;
reconsider y = T `2 as Element of Trees D2 by TREES_3:def 7;
take y ; :: thesis: S1[i,y]
take T ; :: thesis: ( T = p . i & y = T `2 )
thus ( T = p . i & y = T `2 ) ; :: thesis: verum
end;
consider p2 being FinSequence of Trees D2 such that
A3: ( dom p2 = Seg (len p) & ( for i being Nat st i in Seg (len p) holds
S1[i,p2 . i] ) ) from take p2 ; :: thesis: ( dom p2 = dom p & ( for i being Nat st i in dom p holds
ex T being Element of F st
( T = p . i & p2 . i = T `2 ) ) & ([d1,d2] -tree p) `2 = d2 -tree p2 )

thus A4: dom p2 = dom p by ; :: thesis: ( ( for i being Nat st i in dom p holds
ex T being Element of F st
( T = p . i & p2 . i = T `2 ) ) & ([d1,d2] -tree p) `2 = d2 -tree p2 )

hence for i being Nat st i in dom p holds
ex T being Element of F st
( T = p . i & p2 . i = T `2 ) by A3; :: thesis: ([d1,d2] -tree p) `2 = d2 -tree p2
now :: thesis: 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
let i be Nat; :: thesis: ( i in dom p implies for T being DecoratedTree of D1,D2 st T = p . i holds
p2 . i = T `2 )

assume i in dom p ; :: thesis: for T being DecoratedTree of D1,D2 st T = p . i holds
p2 . i = T `2

then ex T being Element of F st
( T = p . i & p2 . i = T `2 ) by A3, A4;
hence for T being DecoratedTree of D1,D2 st T = p . i holds
p2 . i = T `2 ; :: thesis: verum
end;
hence ([d1,d2] -tree p) `2 = d2 -tree p2 by ; :: thesis: verum