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 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; 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; 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; 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; 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 S1[ 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 S1[i,x]
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
S1[i,p2 . i] ) )
from FINSEQ_1:sch 5(A2);
take
p2
; ( 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; ( ( 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; ([d1,d2] -tree p) `2 = d2 -tree p2
hence
([d1,d2] -tree p) `2 = d2 -tree p2
by A4, Th28; verum