reconsider f = I --> {{} } as Function ;
dom f = I by FUNCOP_1:19;
then reconsider f = f as ManySortedSet of I by PBOOLE:def 3;
take f ; :: thesis: ( f is non-empty & f is locally-finite )
thus f is non-empty ; :: thesis: f is locally-finite
thus f is locally-finite :: thesis: verum

proof

let i be set ; :: according to PRE_CIRC:def 3 :: thesis: ( i in I implies f . i is finite )
assume i in I ; :: thesis: f . i is finite
hence f . i is finite by FUNCOP_1:13; :: thesis: verum

end;