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 p2 being FinSequence of FinTrees D2 st
( dom p2 = 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 & 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 p being FinSequence of FinTrees [:D1,D2:] ex p2 being FinSequence of FinTrees D2 st
( dom p2 = 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 & p2 . i = T `2 ) ) & ([d1,d2] -tree p) `2 = d2 -tree p2 )
let d2 be Element of D2; :: thesis: for p being FinSequence of FinTrees [:D1,D2:] ex p2 being FinSequence of FinTrees D2 st
( dom p2 = 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 & p2 . i = T `2 ) ) & ([d1,d2] -tree p) `2 = d2 -tree p2 )
let p be FinSequence of FinTrees [:D1,D2:]; :: thesis: ex p2 being FinSequence of FinTrees D2 st
( dom p2 = 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 & 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 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 & p2 . i = T `2 ) and
A3: ([d1,d2] -tree p) `2 = d2 -tree p2 by Th30;
rng p2 c= FinTrees D2

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p2 or x in FinTrees D2 )
assume x in rng p2 ; :: thesis: x in FinTrees D2
then consider y being set such that
A4: ( y in dom p2 & x = p2 . 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 & p2 . y = T `2 ) by A1, A2, A4;
( dom T is finite & dom (T `2 ) = dom T ) by Th24;
hence x in FinTrees D2 by A4, A5, TREES_3:def 8; :: thesis: verum

end;

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 Element of 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, A3; :: thesis: verum