let a be Real_Sequence; :: according to RCOMP_1:def 4 :: thesis: ( not K2(a) c= {} REAL or not a is convergent or lim a in {} REAL )
assume that
A1: rng a c= {} REAL and
a is convergent ; :: thesis: lim a in {} REAL
rng a = {} by A1, XBOOLE_1:3;
then dom a = {} ;
hence lim a in {} REAL ; :: thesis: verum