reconsider f = <*{}*> as FinSequence ;
take f ; :: thesis: f is V40()
now :: thesis: for x being set st x in rng f holds
x is finite
let x be set ; :: thesis: ( x in rng f implies x is finite )
assume x in rng f ; :: thesis: x is finite
then x in {{}} by FINSEQ_1:39;
hence x is finite ; :: thesis: verum
end;
hence f is V40() ; :: thesis: verum