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

proof

let x be object ; :: 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 ex f being Function st
( x = f & dom f = T & rng f c= D ) by FUNCT_2:def 2;
hence x is DecoratedTree by TREES_2:def 8; :: thesis: verum

end;

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

proof

let x be object ; :: 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 ex f being Function st
( x = f & dom f = T & rng f c= D ) by FUNCT_2:def 2;
hence x is DecoratedTree of D by RELAT_1:def 19, TREES_2:def 8; :: thesis: verum

end;

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