let D1, D2 be non empty set ; 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; 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; 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; 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; 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]
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
; ( 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; ( ( 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; ([d1,d2] -tree p) `1 = d1 -tree p1
hence
([d1,d2] -tree p) `1 = d1 -tree p1
by A4, Th27; verum