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 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 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 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 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 & ( for i being Nat st i in dom p holds
ex T being Element of FinTrees [:D1,D2:] st
( T = p . i & p1 . i = T `1 ) ) ) and
A2: ([d1,d2] -tree p) `1 = d1 -tree p1 by Th29;
rng p1 c= FinTrees D1
proof
let x be object ; :: 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 object such that
A3: y in dom p1 and
A4: x = p1 . 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: p1 . y = T `1 by A1, A3;
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 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; :: thesis: verum