let ts be FinSequence of T; :: thesis: ts is DTree-yielding

now

let x be set ; :: thesis: ( x in dom ts implies ts . x is DecoratedTree )
assume x in dom ts ; :: thesis: ts . x is DecoratedTree
then ts . x in T by Th2;
hence ts . x is DecoratedTree by TREES_3:def 5; :: thesis: verum

end;

hence ts is DTree-yielding by TREES_3:26; :: thesis: verum