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