( 0 |-> T = {} & ( n = 0 or n <> 0 ) ) by FINSEQ_2:72;
hence n |-> T is DTree-yielding by Th38; :: thesis: verum