let D1, D2 be non empty set ; :: thesis: for d1 being Element of D1
for d2 being Element of D2
for p being FinSequence of FinTrees [:D1,D2:] ex p1 being FinSequence of FinTrees D1 st
( dom p1 = dom p & ( for i being Element of NAT st i in dom p holds
ex T being Element of FinTrees [:D1,D2:] 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 p being FinSequence of FinTrees [:D1,D2:] ex p1 being FinSequence of FinTrees D1 st
( dom p1 = dom p & ( for i being Element of NAT st i in dom p holds
ex T being Element of FinTrees [:D1,D2:] st
( T = p . i & p1 . i = T `1 ) ) & ([d1,d2] -tree p) `1 = d1 -tree p1 )
let d2 be Element of D2; :: thesis: for p being FinSequence of FinTrees [:D1,D2:] ex p1 being FinSequence of FinTrees D1 st
( dom p1 = dom p & ( for i being Element of NAT st i in dom p holds
ex T being Element of FinTrees [:D1,D2:] st
( T = p . i & p1 . i = T `1 ) ) & ([d1,d2] -tree p) `1 = d1 -tree p1 )
let p be FinSequence of FinTrees [:D1,D2:]; :: thesis: ex p1 being FinSequence of FinTrees D1 st
( dom p1 = dom p & ( for i being Element of NAT st i in dom p holds
ex T being Element of FinTrees [:D1,D2:] st
( T = p . i & p1 . i = T `1 ) ) & ([d1,d2] -tree p) `1 = d1 -tree p1 )
consider p1 being FinSequence of Trees D1 such that
A1: dom p1 = dom p and
A2: for i being Element of NAT st i in dom p holds
ex T being Element of FinTrees [:D1,D2:] st
( T = p . i & p1 . i = T `1 ) and
A3: ([d1,d2] -tree p) `1 = d1 -tree p1 by Th29;
rng p1 c= FinTrees D1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p1 or x in FinTrees D1 )
assume x in rng p1 ; :: thesis: x in FinTrees D1
then consider y being set such that
A4: ( y in dom p1 & x = p1 . y ) by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A4;
consider T being Element of FinTrees [:D1,D2:] such that
A5: ( T = p . y & p1 . y = T `1 ) by A1, A2, A4;
( dom T is finite & dom (T `1 ) = dom T ) by Th24;
hence x in FinTrees D1 by A4, A5, TREES_3:def 8; :: thesis: verum

end;

then p1 is FinSequence of FinTrees D1 by FINSEQ_1:def 4;
hence ex p1 being FinSequence of FinTrees D1 st
( dom p1 = dom p & ( for i being Element of NAT st i in dom p holds
ex T being Element of FinTrees [:D1,D2:] st
( T = p . i & p1 . i = T `1 ) ) & ([d1,d2] -tree p) `1 = d1 -tree p1 ) by A1, A2, A3; :: thesis: verum