now :: thesis: for y being object st y in rng <*x*> holds
y in ExtREAL
let y be object ; :: thesis: ( y in rng <*x*> implies y in ExtREAL )
assume y in rng <*x*> ; :: thesis: y in ExtREAL
then y in {x} by FINSEQ_1:39;
hence y in ExtREAL by XXREAL_0:def 1; :: thesis: verum
end;
hence <*x*> is FinSequence of ExtREAL by TARSKI:def 3, FINSEQ_1:def 4; :: thesis: verum