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