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

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

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

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

( 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

proof

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

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

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

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

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

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

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

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

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

S

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

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