0 |-> T = {} ;
hence n |-> T is FinTree-yielding by Th35; :: thesis: verum