rng rf c= REAL ;
hence rf is FinSequence of F_Real by FINSEQ_1:def 4; :: thesis: verum