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