for y being object st y in rng <*x*> holds
y in ExtREAL ;
hence <*x*> is FinSequence of ExtREAL by FINSEQ_1:def 4; :: thesis: verum