let D1, D2 be non empty set ; for d1 being Element of D1
for d2 being Element of D2
for p being FinSequence of FinTrees [:D1,D2:] ex p2 being FinSequence of FinTrees D2 st
( dom p2 = dom p & ( for i being Nat st i in dom p holds
ex T being Element of FinTrees [:D1,D2:] 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 p being FinSequence of FinTrees [:D1,D2:] ex p2 being FinSequence of FinTrees D2 st
( dom p2 = dom p & ( for i being Nat st i in dom p holds
ex T being Element of FinTrees [:D1,D2:] st
( T = p . i & p2 . i = T `2 ) ) & ([d1,d2] -tree p) `2 = d2 -tree p2 )
let d2 be Element of D2; for p being FinSequence of FinTrees [:D1,D2:] ex p2 being FinSequence of FinTrees D2 st
( dom p2 = dom p & ( for i being Nat st i in dom p holds
ex T being Element of FinTrees [:D1,D2:] st
( T = p . i & p2 . i = T `2 ) ) & ([d1,d2] -tree p) `2 = d2 -tree p2 )
let p be FinSequence of FinTrees [:D1,D2:]; ex p2 being FinSequence of FinTrees D2 st
( dom p2 = dom p & ( for i being Nat st i in dom p holds
ex T being Element of FinTrees [:D1,D2:] st
( T = p . i & p2 . i = T `2 ) ) & ([d1,d2] -tree p) `2 = d2 -tree p2 )
consider p2 being FinSequence of Trees D2 such that
A1:
( dom p2 = dom p & ( for i being Nat st i in dom p holds
ex T being Element of FinTrees [:D1,D2:] st
( T = p . i & p2 . i = T `2 ) ) )
and
A2:
([d1,d2] -tree p) `2 = d2 -tree p2
by Th30;
rng p2 c= FinTrees D2
then
p2 is FinSequence of FinTrees D2
by FINSEQ_1:def 4;
hence
ex p2 being FinSequence of FinTrees D2 st
( dom p2 = dom p & ( for i being Nat st i in dom p holds
ex T being Element of FinTrees [:D1,D2:] st
( T = p . i & p2 . i = T `2 ) ) & ([d1,d2] -tree p) `2 = d2 -tree p2 )
by A1, A2; verum