reconsider f = I --> {{}} as Function ;
reconsider f = f as ManySortedSet of I ;
take f ; :: thesis: ( f is V2() & f is V41() )
thus f is V2() ; :: thesis: f is V41()
thus f is V41() :: thesis: verum

proof

let i be set ; :: according to FINSET_1:def 5 :: 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;