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 S₁[ 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 S₁[i,x]

proof

let i be Nat; :: thesis: ( i in Seg (len p) implies ex x being Element of Trees D2 st S₁[i,x] )
assume i in Seg (len p) ; :: thesis: ex x being Element of Trees D2 st S₁[i,x]
then reconsider T = p . i as Element of F by A1, Lm1;
reconsider y = T `2 as Element of Trees D2 by TREES_3:def 7;
take y ; :: thesis: S<sub>1</sub>[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
S₁[i,p2 . i] ) ) from FINSEQ_1:sch 5(A2);
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 A3, FINSEQ_1:def 3; :: 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 A4, Th28; :: thesis: verum