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