set T = TOP-REAL n;
set E = Euclid n;
set TE = TopSpaceMetr (Euclid n);
A1: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
A2: n in NAT by ORDINAL1:def 12;
thus TOP-REAL n is add-continuous :: thesis: TOP-REAL n is Mult-continuous

proof

let x1, x2 be Point of (TOP-REAL n); :: according to RLTOPSP1:def 8 :: thesis: for b₁ being Element of bool the carrier of (TOP-REAL n) holds
( not b₁ is open or not x1 + x2 in b₁ or ex b₂, b₃ being Element of bool the carrier of (TOP-REAL n) st
( b₂ is open & b₃ is open & x1 in b₂ & x2 in b₃ & b₂ + b₃ c= b₁ ) )
let V be Subset of (TOP-REAL n); :: thesis: ( not V is open or not x1 + x2 in V or ex b₁, b₂ being Element of bool the carrier of (TOP-REAL n) st
( b₁ is open & b₂ is open & x1 in b₁ & x2 in b₂ & b₁ + b₂ c= V ) )
assume that
A3: V is open and
A4: x1 + x2 in V ; :: thesis: ex b₁, b₂ being Element of bool the carrier of (TOP-REAL n) st
( b₁ is open & b₂ is open & x1 in b₁ & x2 in b₂ & b₁ + b₂ c= V )
reconsider X1 = x1, X2 = x2, X12 = x1 + x2 as Point of (Euclid n) by A1, TOPMETR:12;
reconsider v = V as Subset of (TopSpaceMetr (Euclid n)) by A1;
V in the topology of (TOP-REAL n) by A3, PRE_TOPC:def 2;
then v is open by A1, PRE_TOPC:def 2;
then consider r being real number such that
A5: r > 0 and
A6: Ball (X12,r) c= v by A4, TOPMETR:15;
set r2 = r / 2;
reconsider B1 = Ball (X1,(r / 2)), B2 = Ball (X2,(r / 2)) as Subset of (TOP-REAL n) by A1, TOPMETR:12;
take B1 ; :: thesis: ex b₁ being Element of bool the carrier of (TOP-REAL n) st
( B1 is open & b₁ is open & x1 in B1 & x2 in b₁ & B1 + b₁ 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 A2, A5, GOBOARD6:1, GOBOARD6:3, XREAL_1:215; :: thesis: B1 + B2 c= V
let x be set ; :: 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 (TOP-REAL n) : ( b1 in B1 & b2 in B2 ) } by RUSUB_4:def 9;
then consider b1, b2 being Element of (TOP-REAL n) such that
A7: x = b1 + b2 and
A8: b1 in B1 and
A9: b2 in B2 ;
reconsider e1 = b1, e2 = b2, e12 = b1 + b2 as Point of (Euclid n) by A1, TOPMETR:12;
reconsider y1 = x1, y2 = x2, c1 = b1, c2 = b2 as Element of REAL n by EUCLID:22;
dist (X2,e2) < r / 2 by A9, METRIC_1:11;
then A10: |.(y2 - c2).| < r / 2 by A2, SPPOL_1:5;
dist (X1,e1) < r / 2 by A8, METRIC_1:11;
then |.(y1 - c1).| < r / 2 by A2, SPPOL_1:5;
then A11: |.(y1 - c1).| + |.(y2 - c2).| < (r / 2) + (r / 2) by A10, XREAL_1:8;
A12: (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 ;
A13: dist (X12,e12) = |.((y1 - c1) + (y2 - c2)).| by A2, A12, SPPOL_1:5;
|.((y1 - c1) + (y2 - c2)).| <= |.(y1 - c1).| + |.(y2 - c2).| by EUCLID:12;
then dist (X12,e12) < r by A11, A13, XXREAL_0:2;
then e12 in Ball (X12,r) by METRIC_1:11;
hence x in V by A6, A7; :: thesis: verum

end;

let a be Real; :: according to RLTOPSP1:def 9 :: thesis: for b₁ being Element of the carrier of (TOP-REAL n)
for b₂ being Element of bool the carrier of (TOP-REAL n) holds
( not b₂ is open or not a * b₁ in b₂ or ex b₃ being Element of REAL ex b₄ being Element of bool the carrier of (TOP-REAL n) st
( b₄ is open & b₁ in b₄ & ( for b₅ being Element of REAL holds
( b₃ <= abs (b₅ - a) or b₅ * b₄ c= b₂ ) ) ) )
let x be Point of (TOP-REAL n); :: thesis: for b₁ being Element of bool the carrier of (TOP-REAL n) holds
( not b₁ is open or not a * x in b₁ or ex b₂ being Element of REAL ex b₃ being Element of bool the carrier of (TOP-REAL n) st
( b₃ is open & x in b₃ & ( for b₄ being Element of REAL holds
( b₂ <= abs (b₄ - a) or b₄ * b₃ c= b₁ ) ) ) )
let V be Subset of (TOP-REAL n); :: thesis: ( not V is open or not a * x in V or ex b₁ being Element of REAL ex b₂ being Element of bool the carrier of (TOP-REAL n) st
( b₂ is open & x in b₂ & ( for b₃ being Element of REAL holds
( b₁ <= abs (b₃ - a) or b₃ * b₂ c= V ) ) ) )
assume that
A14: V is open and
A15: a * x in V ; :: thesis: ex b₁ being Element of REAL ex b₂ being Element of bool the carrier of (TOP-REAL n) st
( b₂ is open & x in b₂ & ( for b₃ being Element of REAL holds
( b₁ <= abs (b₃ - a) or b₃ * b₂ c= V ) ) )
reconsider X = x, AX = a * x as Point of (Euclid n) by A1, TOPMETR:12;
reconsider v = V as Subset of (TopSpaceMetr (Euclid n)) by A1;
V in the topology of (TOP-REAL n) by A14, PRE_TOPC:def 2;
then v is open by A1, PRE_TOPC:def 2;
then consider r being real number such that
A16: r > 0 and
A17: Ball (AX,r) c= v by A15, TOPMETR:15;
set r2 = r / 2;
A18: r / 2 > 0 by A16, XREAL_1:215;
then A19: (r / 2) / 2 > 0 by XREAL_1:215;
ex m being positive Real st (abs a) * m < r / 2

proof

per cases ( abs a = 0 or abs a > 0 ) by COMPLEX1:46;

suppose abs a = 0 ; :: thesis: ex m being positive Real st (abs a) * m < r / 2

then (abs a) * 1 < r / 2 by A16, XREAL_1:215;
hence ex m being positive Real st (abs a) * m < r / 2 ; :: thesis: verum

end;

suppose A20: abs a > 0 ; :: thesis: ex m being positive Real st (abs a) * m < r / 2

then reconsider m = ((r / 2) / 2) / (abs a) as positive Real by A19, XREAL_1:139;
take m ; :: thesis: (abs a) * m < r / 2
(r / 2) / 2 < r / 2 by A16, XREAL_1:215, XREAL_1:216;
hence (abs a) * m < r / 2 by A20, XCMPLX_1:87; :: thesis: verum

end;

end;

end;

then consider m being positive Real such that
A21: (abs a) * m < r / 2 ;
reconsider B = Ball (X,m) as Subset of (TOP-REAL n) by A1, TOPMETR:12;
reconsider nr = (r / 2) / (|.x.| + m) as positive Real by A18, XREAL_1:139;
take nr ; :: thesis: ex b₁ being Element of bool the carrier of (TOP-REAL n) st
( b₁ is open & x in b₁ & ( for b₂ being Element of REAL holds
( nr <= abs (b₂ - a) or b₂ * b₁ c= V ) ) )
take B ; :: thesis: ( B is open & x in B & ( for b₁ being Element of REAL holds
( nr <= abs (b₁ - a) or b₁ * B c= V ) ) )
thus ( B is open & x in B ) by A2, GOBOARD6:1, GOBOARD6:3; :: thesis: for b₁ being Element of REAL holds
( nr <= abs (b₁ - a) or b₁ * B c= V )
let s be Real; :: thesis: ( nr <= abs (s - a) or s * B c= V )
assume A22: abs (s - a) < nr ; :: thesis: s * B c= V
let z be set ; :: 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 (TOP-REAL n) : b in B } by CONVEX1:def 1;
then consider b being Element of (TOP-REAL n) such that
A23: z = s * b and
A24: b in B ;
reconsider e = b, se = s * b as Point of (Euclid n) by A1, TOPMETR:12;
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 A25: |.c.| <= |.(c - y).| + |.y.| by EUCLID:12;
A26: dist (X,e) < m by A24, METRIC_1:11;
then |.(c - y).| < m by A2, SPPOL_1:5;
then |.(c - y).| + |.y.| <= m + |.x.| by XREAL_1:6;
then |.c.| <= m + |.x.| by A25, XXREAL_0:2;
then A27: 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 A28: |.((a * y) + (- (a * c))).| = (abs a) * |.(y - c).| by EUCLID:11;
( abs a >= 0 & |.(y - c).| = dist (X,e) ) by A2, COMPLEX1:46, SPPOL_1:5;
then |.((a * y) + (- (a * c))).| <= (abs a) * m by A26, A28, XREAL_1:64;
then A29: |.((a * y) + (- (a * c))).| < r / 2 by A21, XXREAL_0:2;
(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))).| = (abs (a - s)) * |.c.| by EUCLID:11
.= (abs (- (a - s))) * |.c.| by COMPLEX1:52 ;
then ( nr * (|.x.| + m) = r / 2 & |.((a * c) + (- (s * c))).| <= nr * |.c.| ) by A22, XCMPLX_1:87, XREAL_1:64;
then |.((a * c) + (- (s * c))).| <= r / 2 by A27, XXREAL_0:2;
then A30: ( |.(((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 A29, EUCLID:12, XREAL_1:8;
(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 A2, SPPOL_1:5;
then dist (AX,se) < r by A30, XXREAL_0:2;
then se in Ball (AX,r) by METRIC_1:11;
hence z in V by A17, A23; :: thesis: verum