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