set A = { (Funcs (T,D)) where T is Element of Trees : verum } ;
set TT = union { (Funcs (T,D)) where T is Element of Trees : verum } ;
set f = the Element of Trees --> the Element of D;
A1: the Element of Trees --> the Element of D in Funcs ( the Element of Trees ,D) by FUNCT_2:8;
A2: Funcs ( the Element of Trees ,D) in { (Funcs (T,D)) where T is Element of Trees : verum } ;
union { (Funcs (T,D)) where T is Element of Trees : verum } is constituted-DTrees

proof

let x be object ; :: according to TREES_3:def 5 :: thesis: ( x in union { (Funcs (T,D)) where T is Element of Trees : verum } implies x is DecoratedTree )
assume x in union { (Funcs (T,D)) where T is Element of Trees : verum } ; :: thesis: x is DecoratedTree
then consider X being set such that
A3: x in X and
A4: X in { (Funcs (T,D)) where T is Element of Trees : verum } by TARSKI:def 4;
ex T being Element of Trees st X = Funcs (T,D) by A4;
hence x is DecoratedTree by A3; :: thesis: verum

end;

then reconsider TT = union { (Funcs (T,D)) where T is Element of Trees : verum } as non empty constituted-DTrees set by A2, A1, TARSKI:def 4;
TT is DTree-set of D

proof

let x be object ; :: according to TREES_3:def 6 :: thesis: ( x in TT implies x is DecoratedTree of D )
assume x in TT ; :: thesis: x is DecoratedTree of D
then consider X being set such that
A5: x in X and
A6: X in { (Funcs (T,D)) where T is Element of Trees : verum } by TARSKI:def 4;
ex T being Element of Trees st X = Funcs (T,D) by A6;
hence x is DecoratedTree of D by A5; :: thesis: verum

end;

then reconsider TT = TT as DTree-set of D ;
take TT ; :: thesis: for T being DecoratedTree of D holds T in TT
let T be DecoratedTree of D; :: thesis: T in TT
reconsider t = dom T as Element of Trees by Def1;
rng T c= D ;
then A7: T in Funcs (t,D) by FUNCT_2:def 2;
Funcs (t,D) in { (Funcs (W,D)) where W is Element of Trees : verum } ;
hence T in TT by A7, TARSKI:def 4; :: thesis: verum