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 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 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 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 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

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; :: thesis: verum

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; :: 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 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 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 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

proof

then
p2 is FinSequence of FinTrees D2
by FINSEQ_1:def 4;
let x be object ; :: 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 object such that

A3: y in dom p2 and

A4: x = p2 . y by FUNCT_1:def 3;

reconsider y = y as Nat by A3;

consider T being Element of FinTrees [:D1,D2:] such that

T = p . y and

A5: p2 . y = T `2 by A1, A3;

dom (T `2) = dom T by Th24;

hence x in FinTrees D2 by A4, A5, TREES_3:def 8; :: thesis: verum

end;assume x in rng p2 ; :: thesis: x in FinTrees D2

then consider y being object such that

A3: y in dom p2 and

A4: x = p2 . y by FUNCT_1:def 3;

reconsider y = y as Nat by A3;

consider T being Element of FinTrees [:D1,D2:] such that

T = p . y and

A5: p2 . y = T `2 by A1, A3;

dom (T `2) = dom T by Th24;

hence x in FinTrees D2 by A4, A5, TREES_3:def 8; :: thesis: verum

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; :: thesis: verum