let q3 be Real; :: thesis: for X being Subset of REAL st X is closed holds
q3 ++ X is closed
let X be Subset of REAL; :: thesis: ( X is closed implies q3 ++ X is closed )
assume A1: X is closed ; :: thesis: q3 ++ X is closed
AA: q3 ++ X = { (q3 + r3) where r3 is Real : r3 in X } by LmX;
reconsider s0 = NAT --> q3 as Real_Sequence ;
let s1 be Real_Sequence; :: according to RCOMP_1:def 4 :: thesis: ( not proj2 s1 c= q3 ++ X or not s1 is convergent or lim s1 in q3 ++ X )
assume that
A2: rng s1 c= q3 ++ X and
A3: s1 is convergent ; :: thesis: lim s1 in q3 ++ X
lim (s1 - s0) = (lim s1) - (s0 . 0) by A3, SEQ_4:59
.= (lim s1) - q3 by FUNCOP_1:13 ;
then A4: q3 + (lim (s1 - s0)) = lim s1 ;
A5: rng (s1 - s0) c= X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (s1 - s0) or x in X )
assume A6: x in rng (s1 - s0) ; :: thesis: x in X
then consider n being set such that
A7: n in dom (s1 - s0) and
A8: x = (s1 - s0) . n by FUNCT_1:def 5;
reconsider x9 = x as Real by A6;
reconsider n = n as Element of NAT by A7;
A9: s1 . n in rng s1 by FUNCT_2:6;
x = (s1 . n) + ((- s0) . n) by A8, SEQ_1:11
.= (s1 . n) + (- (s0 . n)) by SEQ_1:14
.= (s1 . n) - q3 by FUNCOP_1:13 ;
then x9 + q3 in q3 ++ X by A2, A9;
hence x in X by Th20; :: thesis: verum

end;

s1 - s0 is convergent by A3, SEQ_2:25;
then lim (s1 - s0) in X by A1, A5, RCOMP_1:def 4;
hence lim s1 in q3 ++ X by A4, AA; :: thesis: verum