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