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