let F be FinSequence of REAL ; :: thesis: F is FinSequence of ExtREAL
rng F c= ExtREAL by NUMBERS:31, XBOOLE_1:1;
hence F is FinSequence of ExtREAL by FINSEQ_1:def 4; :: thesis: verum