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:32;
hence seq is Real_Sequence by FUNCT_2:6; :: thesis: verum