set T = TOP-REAL n;
set E = Euclid n;
set TE = TopSpaceMetr ();
A1: TopStruct(# the carrier of (), the topology of () #) = TopSpaceMetr () by EUCLID:def 8;
thus TOP-REAL n is add-continuous :: thesis:
proof
let x1, x2 be Point of (); :: according to RLTOPSP1:def 8 :: thesis: for b1 being Element of bool the carrier of () holds
( not b1 is open or not x1 + x2 in b1 or ex b2, b3 being Element of bool the carrier of () st
( b2 is open & b3 is open & x1 in b2 & x2 in b3 & b2 + b3 c= b1 ) )

let V be Subset of (); :: thesis: ( not V is open or not x1 + x2 in V or ex b1, b2 being Element of bool the carrier of () st
( b1 is open & b2 is open & x1 in b1 & x2 in b2 & b1 + b2 c= V ) )

assume that
A2: V is open and
A3: x1 + x2 in V ; :: thesis: ex b1, b2 being Element of bool the carrier of () st
( b1 is open & b2 is open & x1 in b1 & x2 in b2 & b1 + b2 c= V )

reconsider X1 = x1, X2 = x2, X12 = x1 + x2 as Point of () by ;
reconsider v = V as Subset of () by A1;
V in the topology of () by ;
then v is open by ;
then consider r being Real such that
A4: r > 0 and
A5: Ball (X12,r) c= v by ;
set r2 = r / 2;
reconsider B1 = Ball (X1,(r / 2)), B2 = Ball (X2,(r / 2)) as Subset of () by ;
take B1 ; :: thesis: ex b1 being Element of bool the carrier of () st
( B1 is open & b1 is open & x1 in B1 & x2 in b1 & B1 + b1 c= V )

take B2 ; :: thesis: ( B1 is open & B2 is open & x1 in B1 & x2 in B2 & B1 + B2 c= V )
thus ( B1 is open & B2 is open & x1 in B1 & x2 in B2 ) by ; :: thesis: B1 + B2 c= V
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B1 + B2 or x in V )
assume x in B1 + B2 ; :: thesis: x in V
then x in { (b1 + b2) where b1, b2 is Element of () : ( b1 in B1 & b2 in B2 ) } by RUSUB_4:def 9;
then consider b1, b2 being Element of () such that
A6: x = b1 + b2 and
A7: b1 in B1 and
A8: b2 in B2 ;
reconsider e1 = b1, e2 = b2, e12 = b1 + b2 as Point of () by ;
reconsider y1 = x1, y2 = x2, c1 = b1, c2 = b2 as Element of REAL n by EUCLID:22;
dist (X2,e2) < r / 2 by ;
then A9: |.(y2 - c2).| < r / 2 by SPPOL_1:5;
dist (X1,e1) < r / 2 by ;
then |.(y1 - c1).| < r / 2 by SPPOL_1:5;
then A10: |.(y1 - c1).| + |.(y2 - c2).| < (r / 2) + (r / 2) by ;
A11: (y1 + y2) - (c1 + c2) = (y1 + y2) + (- (c2 + c1)) by RVSUM_1:31
.= (y1 + y2) + ((- c2) + (- c1)) by RVSUM_1:26
.= ((y1 + y2) + (- c2)) + (- c1) by RVSUM_1:15
.= ((y2 + (- c2)) + y1) + (- c1) by RVSUM_1:15
.= (y2 + (- c2)) + (y1 + (- c1)) by RVSUM_1:15
.= (y2 - c2) + (y1 + (- c1)) by RVSUM_1:31
.= (y2 - c2) + (y1 - c1) by RVSUM_1:31 ;
A12: dist (X12,e12) = |.((y1 - c1) + (y2 - c2)).| by ;
|.((y1 - c1) + (y2 - c2)).| <= |.(y1 - c1).| + |.(y2 - c2).| by EUCLID:12;
then dist (X12,e12) < r by ;
then e12 in Ball (X12,r) by METRIC_1:11;
hence x in V by A5, A6; :: thesis: verum
end;
let a be Real; :: according to RLTOPSP1:def 9 :: thesis: for b1 being Element of the carrier of ()
for b2 being Element of bool the carrier of () holds
( not b2 is open or not a * b1 in b2 or ex b3 being object ex b4 being Element of bool the carrier of () st
( b4 is open & b1 in b4 & ( for b5 being object holds
( b3 <= |.(b5 - a).| or b5 * b4 c= b2 ) ) ) )

let x be Point of (); :: thesis: for b1 being Element of bool the carrier of () holds
( not b1 is open or not a * x in b1 or ex b2 being object ex b3 being Element of bool the carrier of () st
( b3 is open & x in b3 & ( for b4 being object holds
( b2 <= |.(b4 - a).| or b4 * b3 c= b1 ) ) ) )

let V be Subset of (); :: thesis: ( not V is open or not a * x in V or ex b1 being object ex b2 being Element of bool the carrier of () st
( b2 is open & x in b2 & ( for b3 being object holds
( b1 <= |.(b3 - a).| or b3 * b2 c= V ) ) ) )

assume that
A13: V is open and
A14: a * x in V ; :: thesis: ex b1 being object ex b2 being Element of bool the carrier of () st
( b2 is open & x in b2 & ( for b3 being object holds
( b1 <= |.(b3 - a).| or b3 * b2 c= V ) ) )

reconsider X = x, AX = a * x as Point of () by ;
reconsider v = V as Subset of () by A1;
V in the topology of () by ;
then v is open by ;
then consider r being Real such that
A15: r > 0 and
A16: Ball (AX,r) c= v by ;
set r2 = r / 2;
A17: r / 2 > 0 by ;
then A18: (r / 2) / 2 > 0 by XREAL_1:215;
ex m being positive Real st |.a.| * m < r / 2
proof
per cases = 0 or |.a.| > 0 ) by COMPLEX1:46;
suppose |.a.| = 0 ; :: thesis: ex m being positive Real st |.a.| * m < r / 2
then |.a.| * 1 < r / 2 by ;
hence ex m being positive Real st |.a.| * m < r / 2 ; :: thesis: verum
end;
suppose A19: |.a.| > 0 ; :: thesis: ex m being positive Real st |.a.| * m < r / 2
then reconsider m = ((r / 2) / 2) / |.a.| as positive Real by ;
take m ; :: thesis: |.a.| * m < r / 2
(r / 2) / 2 < r / 2 by ;
hence |.a.| * m < r / 2 by ; :: thesis: verum
end;
end;
end;
then consider m being positive Real such that
A20: |.a.| * m < r / 2 ;
reconsider B = Ball (X,m) as Subset of () by ;
reconsider nr = (r / 2) / (|.x.| + m) as positive Real by ;
take nr ; :: thesis: ex b1 being Element of bool the carrier of () st
( b1 is open & x in b1 & ( for b2 being object holds
( nr <= |.(b2 - a).| or b2 * b1 c= V ) ) )

take B ; :: thesis: ( B is open & x in B & ( for b1 being object holds
( nr <= |.(b1 - a).| or b1 * B c= V ) ) )

thus ( B is open & x in B ) by ; :: thesis: for b1 being object holds
( nr <= |.(b1 - a).| or b1 * B c= V )

let s be Real; :: thesis: ( nr <= |.(s - a).| or s * B c= V )
assume A21: |.(s - a).| < nr ; :: thesis: s * B c= V
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in s * B or z in V )
assume z in s * B ; :: thesis: z in V
then z in { (s * b) where b is Element of () : b in B } by CONVEX1:def 1;
then consider b being Element of () such that
A22: z = s * b and
A23: b in B ;
reconsider e = b, se = s * b as Point of () by ;
reconsider y = x, c = b as Element of REAL n by EUCLID:22;
reconsider Y = y, C = c as Element of n -tuples_on REAL by EUCLID:def 1;
c = C - (n |-> 0) by RVSUM_1:32
.= C - (Y - Y) by RVSUM_1:37
.= (C - Y) + Y by RVSUM_1:41 ;
then A24: |.c.| <= |.(c - y).| + |.y.| by EUCLID:12;
A25: dist (X,e) < m by ;
then |.(c - y).| < m by SPPOL_1:5;
then |.(c - y).| + |.y.| <= m + |.x.| by XREAL_1:6;
then |.c.| <= m + |.x.| by ;
then A26: nr * |.c.| <= nr * (m + |.x.|) by XREAL_1:64;
(a * y) + (- (a * c)) = (a * y) + ((- 1) * (a * c)) by RVSUM_1:54
.= (a * y) + (((- 1) * a) * c) by RVSUM_1:49
.= (a * y) + (a * ((- 1) * c)) by RVSUM_1:49
.= a * (y + ((- 1) * c)) by RVSUM_1:51
.= a * (y + (- c)) by RVSUM_1:54
.= a * (y - c) by RVSUM_1:31 ;
then A27: |.((a * y) + (- (a * c))).| = |.a.| * |.(y - c).| by EUCLID:11;
( |.a.| >= 0 & |.(y - c).| = dist (X,e) ) by ;
then |.((a * y) + (- (a * c))).| <= |.a.| * m by ;
then A28: |.((a * y) + (- (a * c))).| < r / 2 by ;
(a * c) + (- (s * c)) = (a * c) + ((- 1) * (s * c)) by RVSUM_1:54
.= (a * c) + (((- 1) * s) * c) by RVSUM_1:49
.= (a + ((- 1) * s)) * c by RVSUM_1:50 ;
then |.((a * c) + (- (s * c))).| = |.(a - s).| * |.c.| by EUCLID:11
.= |.(- (a - s)).| * |.c.| by COMPLEX1:52 ;
then ( nr * (|.x.| + m) = r / 2 & |.((a * c) + (- (s * c))).| <= nr * |.c.| ) by ;
then |.((a * c) + (- (s * c))).| <= r / 2 by ;
then A29: ( |.(((a * y) + (- (a * c))) + ((a * c) + (- (s * c)))).| <= |.((a * y) + (- (a * c))).| + |.((a * c) + (- (s * c))).| & |.((a * y) + (- (a * c))).| + |.((a * c) + (- (s * c))).| < (r / 2) + (r / 2) ) by ;
(a * y) - (s * c) = ((a * Y) - (n |-> 0)) - (s * C) by RVSUM_1:32
.= ((a * y) - ((a * C) - (a * C))) - (s * c) by RVSUM_1:37
.= (((a * y) - (a * C)) + (a * C)) - (s * c) by RVSUM_1:41
.= (((a * y) - (a * C)) + (a * C)) + (- (s * c)) by RVSUM_1:31
.= ((a * y) - (a * C)) + ((a * c) + (- (s * c))) by RVSUM_1:15
.= ((a * y) + (- (a * c))) + ((a * c) + (- (s * c))) by RVSUM_1:31 ;
then dist (AX,se) = |.(((a * y) + (- (a * c))) + ((a * c) + (- (s * c)))).| by SPPOL_1:5;
then dist (AX,se) < r by ;
then se in Ball (AX,r) by METRIC_1:11;
hence z in V by ; :: thesis: verum