let seq be ExtREAL_sequence; :: thesis: ( seq is real-valued implies seq is Real_Sequence )
assume seq is real-valued ; :: thesis: seq is Real_Sequence
then rng seq is Subset of REAL by MESFUNC2:35;
hence seq is Real_Sequence by FUNCT_2:8; :: thesis: verum