let f be DTree-yielding Function; :: thesis: ( dom (doms f) = dom f & doms f is Tree-yielding )
A1: dom (doms f) = f " (SubFuncs (rng f)) by FUNCT_6:def 2;
hence dom (doms f) c= dom f by RELAT_1:132; :: 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) :: thesis: doms f is Tree-yielding

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in dom (doms f) )
assume A2: x in dom f ; :: thesis: x in dom (doms f)
then f . x is DecoratedTree by Th26;
hence x in dom (doms f) by A1, A2, FUNCT_6:19; :: thesis: verum

end;

now

let x be set ; :: 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 A3: x in dom f by A1, FUNCT_6:19;
then reconsider g = f . x as DecoratedTree by Th26;
(doms f) . x = dom g by A3, FUNCT_6:22;
hence (doms f) . x is Tree ; :: thesis: verum

end;

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