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 :: thesis: verum

proof

let i be set ; :: according to FINSET_1:def 4 :: thesis: ( not i in I or f . i is finite )
assume i in I ; :: thesis: f . i is finite
hence f . i is finite by FUNCOP_1:7; :: thesis: verum

end;