rng <*x*> c= REAL

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng <*x*> or y in REAL )
assume y in rng <*x*> ; :: thesis: y in REAL
then y in {x} by FINSEQ_1:56;
then y = x by TARSKI:def 1;
hence y in REAL by XREAL_0:def 1; :: thesis: verum

end;

hence <*x*> is FinSequence of REAL by FINSEQ_1:def 4; :: thesis: verum