theorem :: DTCONSTR:6

for T1, T2 being DecoratedTree holds roots <*T1,T2*> = <*(T1 . {}),(T2 . {})*>