reconsider f = I --> {{}} as Function ;
reconsider f = f as ManySortedSet of I ;
take f ; :: thesis: ( f is non-empty & f is finite-yielding )
thus f is non-empty ; :: thesis: f is finite-yielding
thus f is finite-yielding by FUNCOP_1:7; :: thesis: verum