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 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
A3: rng s1 c= q3 ++ X and
A4: s1 is convergent ; :: thesis: lim s1 in q3 ++ X
lim (s1 - s0) = (lim s1) - (s0 . 0) by A4, SEQ_4:42
.= (lim s1) - q3 by FUNCOP_1:7 ;
then A5: q3 + (lim (s1 - s0)) = lim s1 ;
A6: 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 A7: x in rng (s1 - s0) ; :: thesis: x in X
then consider n being set such that
A8: n in dom (s1 - s0) and
A9: x = (s1 - s0) . 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) + ((- s0) . n) by A9, SEQ_1:7
.= (s1 . n) + (- (s0 . n)) by SEQ_1:10
.= (s1 . n) - q3 by FUNCOP_1:7 ;
then x9 + q3 in q3 ++ X by A3, A10;
hence x in X by Th82; :: thesis: verum

end;

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