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 p1 being FinSequence of Trees D1 st
( dom p1 = dom p & ( for i being Nat st i in dom p holds
ex T being Element of F st
( T = p . i & p1 . i = T `1 ) ) & ([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 p being FinSequence of F ex p1 being FinSequence of Trees D1 st
( dom p1 = dom p & ( for i being Nat st i in dom p holds
ex T being Element of F st
( T = p . i & p1 . i = T `1 ) ) & ([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 p being FinSequence of F ex p1 being FinSequence of Trees D1 st
( dom p1 = dom p & ( for i being Nat st i in dom p holds
ex T being Element of F st
( T = p . i & p1 . i = T `1 ) ) & ([d1,d2] -tree p) `1 = d1 -tree p1 )
let F be non empty DTree-set of D1,D2; :: thesis: for p being FinSequence of F ex p1 being FinSequence of Trees D1 st
( dom p1 = dom p & ( for i being Nat st i in dom p holds
ex T being Element of F st
( T = p . i & p1 . i = T `1 ) ) & ([d1,d2] -tree p) `1 = d1 -tree p1 )
let p be FinSequence of F; :: thesis: ex p1 being FinSequence of Trees D1 st
( dom p1 = dom p & ( for i being Nat st i in dom p holds
ex T being Element of F st
( T = p . i & p1 . i = T `1 ) ) & ([d1,d2] -tree p) `1 = d1 -tree p1 )
A1: Seg (len p) = dom p by FINSEQ_1:def 3;
defpred S1[ set , set ] means ex T being Element of F st
( T = p . $1 & $2 = T `1 );
A2: for i being Nat st i in Seg (len p) holds
ex x being Element of Trees D1 st S1[i,x]
proof
let i be Nat; :: thesis: ( i in Seg (len p) implies ex x being Element of Trees D1 st S1[i,x] )
assume i in Seg (len p) ; :: thesis: ex x being Element of Trees D1 st S1[i,x]
then reconsider T = p . i as Element of F by A1, Lm1;
reconsider y = T `1 as Element of Trees D1 by TREES_3:def 7;
take y ; :: thesis: S1[i,y]
take T ; :: thesis: ( T = p . i & y = T `1 )
thus ( T = p . i & y = T `1 ) ; :: thesis: verum
end;
consider p1 being FinSequence of Trees D1 such that
A3: ( dom p1 = Seg (len p) & ( for i being Nat st i in Seg (len p) holds
S1[i,p1 . i] ) ) from FINSEQ_1:sch 5(A2);
 take p1 ; :: thesis: ( dom p1 = dom p & ( for i being Nat st i in dom p holds
ex T being Element of F st
( T = p . i & p1 . i = T `1 ) ) & ([d1,d2] -tree p) `1 = d1 -tree p1 )
thus A4: dom p1 = 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 & p1 . i = T `1 ) ) & ([d1,d2] -tree p) `1 = d1 -tree p1 )
hence for i being Nat st i in dom p holds
ex T being Element of F st
( T = p . i & p1 . i = T `1 ) by A3; :: thesis: ([d1,d2] -tree p) `1 = d1 -tree p1
now :: thesis: 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
let i be Nat; :: thesis: ( i in dom p implies for T being DecoratedTree of D1,D2 st T = p . i holds
p1 . i = T `1 )
assume i in dom p ; :: thesis: for T being DecoratedTree of D1,D2 st T = p . i holds
p1 . i = T `1
then ex T being Element of F st
( T = p . i & p1 . i = T `1 ) by A3, A4;
hence for T being DecoratedTree of D1,D2 st T = p . i holds
p1 . i = T `1 ; :: thesis: verum
end;
hence ([d1,d2] -tree p) `1 = d1 -tree p1 by A4, Th27; :: thesis: verum