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