set t1t2 = <*T1,T2*>;

dom T1 is finite ;

then A1: T1 in FinTrees D by TREES_3:def 8;

dom T2 is finite ;

then A2: T2 in FinTrees D by TREES_3:def 8;

rng <*T1,T2*> = rng (<*T1*> ^ <*T2*>) by FINSEQ_1:def 9

.= (rng <*T1*>) \/ (rng <*T2*>) by FINSEQ_1:31

.= {T1} \/ (rng <*T2*>) by FINSEQ_1:39

.= {T1} \/ {T2} by FINSEQ_1:39

.= {T1,T2} by ENUMSET1:1 ;

then for x being object st x in rng <*T1,T2*> holds

x in FinTrees D by A1, A2, TARSKI:def 2;

then rng <*T1,T2*> c= FinTrees D by TARSKI:def 3;

then reconsider T1T2 = <*T1,T2*> as FinSequence of FinTrees D by FINSEQ_1:def 4;

x -tree (T1,T2) = x -tree T1T2 by TREES_4:def 6;

then dom (x -tree (T1,T2)) is finite ;

hence ( x -tree (T1,T2) is binary & x -tree (T1,T2) is finite & x -tree (T1,T2) is D -valued ) by Th9, FINSET_1:10; :: thesis: verum

dom T1 is finite ;

then A1: T1 in FinTrees D by TREES_3:def 8;

dom T2 is finite ;

then A2: T2 in FinTrees D by TREES_3:def 8;

rng <*T1,T2*> = rng (<*T1*> ^ <*T2*>) by FINSEQ_1:def 9

.= (rng <*T1*>) \/ (rng <*T2*>) by FINSEQ_1:31

.= {T1} \/ (rng <*T2*>) by FINSEQ_1:39

.= {T1} \/ {T2} by FINSEQ_1:39

.= {T1,T2} by ENUMSET1:1 ;

then for x being object st x in rng <*T1,T2*> holds

x in FinTrees D by A1, A2, TARSKI:def 2;

then rng <*T1,T2*> c= FinTrees D by TARSKI:def 3;

then reconsider T1T2 = <*T1,T2*> as FinSequence of FinTrees D by FINSEQ_1:def 4;

x -tree (T1,T2) = x -tree T1T2 by TREES_4:def 6;

then dom (x -tree (T1,T2)) is finite ;

hence ( x -tree (T1,T2) is binary & x -tree (T1,T2) is finite & x -tree (T1,T2) is D -valued ) by Th9, FINSET_1:10; :: thesis: verum