set F = Funcs T,D;
Funcs T,D is constituted-DTrees

proof

let x be set ; :: according to TREES_3:def 5 :: thesis: ( x in Funcs T,D implies x is DecoratedTree )
assume x in Funcs T,D ; :: thesis: x is DecoratedTree
then consider f being Function such that
A1: ( x = f & dom f = T & rng f c= D ) by FUNCT_2:def 2;
thus x is DecoratedTree by A1, TREES_2:def 8; :: thesis: verum

end;

then reconsider F = Funcs T,D as constituted-DTrees set ;
F is DTree-set of D

proof

let x be set ; :: according to TREES_3:def 6 :: thesis: ( x in F implies x is DecoratedTree of D )
assume x in F ; :: thesis: x is DecoratedTree of D
then consider f being Function such that
A2: ( x = f & dom f = T & rng f c= D ) by FUNCT_2:def 2;
thus x is DecoratedTree of D by A2, TREES_2:def 8, TREES_2:def 9; :: thesis: verum

end;

then reconsider F = F as DTree-set of D ;
consider d being Function of T,D;
( dom d = T & rng d c= D ) by FUNCT_2:def 1;
then d in F by FUNCT_2:def 2;
hence Funcs T,D is non empty DTree-set of D ; :: thesis: verum