let a be Real_Sequence; :: according to RCOMP_1:def 4 :: thesis: ( not rng a c= {} REAL or not a is convergent or lim a in {} REAL )
assume ( rng a c= {} REAL & a is convergent ) ; :: thesis: lim a in {} REAL
hence lim a in {} REAL ; :: thesis: verum