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
A2: q3 ++ X = { (q3 + r3) where r3 is Real : r3 in X } by Lm5;
reconsider qq3 = q3 as Element of REAL by XREAL_0:def 1;
set s0 = seq_const q3;
let s1 be Real_Sequence; :: according to RCOMP_1:def 4 :: thesis: ( not rng s1 c= q3 ++ X or not s1 is convergent or lim s1 in q3 ++ X )
assume that
A3: rng s1 c= q3 ++ X and
A4: s1 is convergent ; :: thesis: lim s1 in q3 ++ X
lim (s1 - (seq_const q3)) = (lim s1) - ((seq_const q3) . 0) by A4, SEQ_4:42
.= (lim s1) - q3 by SEQ_1:57 ;
then A5: q3 + (lim (s1 - (seq_const q3))) = lim s1 ;
A6: rng (s1 - (seq_const q3)) c= X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (s1 - (seq_const q3)) or x in X )
assume A7: x in rng (s1 - (seq_const q3)) ; :: thesis: x in X
then consider n being object such that
A8: n in dom (s1 - (seq_const q3)) and
A9: x = (s1 - (seq_const q3)) . n by FUNCT_1:def 3;
reconsider x9 = x as Real by A7;
reconsider n = n as Element of NAT by A8;
A10: s1 . n in rng s1 by FUNCT_2:4;
x = (s1 . n) + ((- (seq_const q3)) . n) by A9, SEQ_1:7
.= (s1 . n) + (- ((seq_const q3) . n)) by SEQ_1:10
.= (s1 . n) - q3 by SEQ_1:57 ;
then x9 + q3 in q3 ++ X by A3, A10;
hence x in X by Th46; :: thesis: verum

end;

s1 - (seq_const q3) is convergent by A4;
then lim (s1 - (seq_const q3)) in X by A1, A6;
hence lim s1 in q3 ++ X by A5, A2; :: thesis: verum