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 S_{1}[ 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 S_{1}[i,x]

A3: ( dom p1 = Seg (len p) & ( for i being Nat st i in Seg (len p) holds

S_{1}[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

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 S

( 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 S

proof

consider p1 being FinSequence of Trees D1 such that
let i be Nat; :: thesis: ( i in Seg (len p) implies ex x being Element of Trees D1 st S_{1}[i,x] )

assume i in Seg (len p) ; :: thesis: ex x being Element of Trees D1 st S_{1}[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: S_{1}[i,y]

take T ; :: thesis: ( T = p . i & y = T `1 )

thus ( T = p . i & y = T `1 ) ; :: thesis: verum

end;assume i in Seg (len p) ; :: thesis: ex x being Element of Trees D1 st S

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: S

take T ; :: thesis: ( T = p . i & y = T `1 )

thus ( T = p . i & y = T `1 ) ; :: thesis: verum

A3: ( dom p1 = Seg (len p) & ( for i being Nat st i in Seg (len p) holds

S

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

hence
([d1,d2] -tree p) `1 = d1 -tree p1
by A4, Th27; :: thesis: verumfor 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;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