let rF be real-valued XFinSequence; :: thesis: rF is REAL -valued
rng rF c= REAL by VALUED_0:def 3;
hence rF is REAL -valued by RELAT_1:def 19; :: thesis: verum