let f be DTree-yielding Function; :: thesis: ( dom (doms f) = dom f & doms f is Tree-yielding )
A1: dom (doms f) = dom f by FUNCT_6:def 2;
hence dom (doms f) c= dom f ; :: according to XBOOLE_0:def 10 :: thesis: ( dom f c= dom (doms f) & doms f is Tree-yielding )
thus dom f c= dom (doms f) by A1; :: thesis: doms f is Tree-yielding

now :: thesis: for x being object st x in dom (doms f) holds
(doms f) . x is Tree

let x be object ; :: thesis: ( x in dom (doms f) implies (doms f) . x is Tree )
assume x in dom (doms f) ; :: thesis: (doms f) . x is Tree
then A2: x in dom f by A1;
then reconsider g = f . x as DecoratedTree by Th24;
(doms f) . x = dom g by A2, FUNCT_6:22;
hence (doms f) . x is Tree ; :: thesis: verum

end;

hence doms f is Tree-yielding by Th22; :: thesis: verum