dom <:T1,T2:> = (dom T1) /\ (dom T2) by FUNCT_3:def 7;
hence <:T1,T2:> is DecoratedTree-like ; :: thesis: verum