let f be Function of T,D; :: thesis: f is DecoratedTree-like
thus dom f is Tree by FUNCT_2:def 1; :: according to TREES_2:def 8 :: thesis: verum