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 )
thus ( not rng a c= [#] REAL or not a is convergent or lim a in [#] REAL ) ; :: thesis: verum