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:44
.= {T1} \/ (rng <*T2*>) by FINSEQ_1:56
.= {T1} \/ {T2} by FINSEQ_1:56
.= {T1,T2} by ENUMSET1:41 ;
then for x being set 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 finite binary DecoratedTree of D by Th11, FINSET_1:29; :: thesis: verum