reconsider T1 = T1, T2 = T2 as Element of Trees D by TREES_3:def 7;
<*T1,T2*> = <*T1*> ^ <*T2*> ;
then reconsider t = <*T1,T2*> as Element of (Trees D) * by FINSEQ_1:def 11;
d -tree (T1,T2) = d -tree t ;
hence d -tree (T1,T2) is D -valued ; :: thesis: verum