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