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