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;

thus TOP-REAL n is add-continuous :: thesis: TOP-REAL n is Mult-continuous_{1} being Element of the carrier of (TOP-REAL n)

for b_{2} being Element of bool the carrier of (TOP-REAL n) holds

( not b_{2} is open or not a * b_{1} in b_{2} or ex b_{3} being object ex b_{4} being Element of bool the carrier of (TOP-REAL n) st

( b_{4} is open & b_{1} in b_{4} & ( for b_{5} being object holds

( b_{3} <= |.(b_{5} - a).| or b_{5} * b_{4} c= b_{2} ) ) ) )

let x be Point of (TOP-REAL n); :: thesis: for b_{1} being Element of bool the carrier of (TOP-REAL n) holds

( not b_{1} is open or not a * x in b_{1} or ex b_{2} being object ex b_{3} being Element of bool the carrier of (TOP-REAL n) st

( b_{3} is open & x in b_{3} & ( for b_{4} being object holds

( b_{2} <= |.(b_{4} - a).| or b_{4} * b_{3} c= b_{1} ) ) ) )

let V be Subset of (TOP-REAL n); :: thesis: ( not V is open or not a * x in V or ex b_{1} being object ex b_{2} being Element of bool the carrier of (TOP-REAL n) st

( b_{2} is open & x in b_{2} & ( for b_{3} being object holds

( b_{1} <= |.(b_{3} - a).| or b_{3} * b_{2} c= V ) ) ) )

assume that

A13: V is open and

A14: a * x in V ; :: thesis: ex b_{1} being object ex b_{2} being Element of bool the carrier of (TOP-REAL n) st

( b_{2} is open & x in b_{2} & ( for b_{3} being object holds

( b_{1} <= |.(b_{3} - a).| or b_{3} * b_{2} 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 A13, PRE_TOPC:def 2;

then v is open by A1, PRE_TOPC:def 2;

then consider r being Real such that

A15: r > 0 and

A16: Ball (AX,r) c= v by A14, TOPMETR:15;

set r2 = r / 2;

A17: r / 2 > 0 by A15, XREAL_1:215;

then A18: (r / 2) / 2 > 0 by XREAL_1:215;

ex m being positive Real st |.a.| * m < r / 2

A20: |.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 A17, XREAL_1:139;

take nr ; :: thesis: ex b_{1} being Element of bool the carrier of (TOP-REAL n) st

( b_{1} is open & x in b_{1} & ( for b_{2} being object holds

( nr <= |.(b_{2} - a).| or b_{2} * b_{1} c= V ) ) )

take B ; :: thesis: ( B is open & x in B & ( for b_{1} being object holds

( nr <= |.(b_{1} - a).| or b_{1} * B c= V ) ) )

thus ( B is open & x in B ) by GOBOARD6:1, GOBOARD6:3; :: thesis: for b_{1} being object holds

( nr <= |.(b_{1} - a).| or b_{1} * 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 (TOP-REAL n) : b in B } by CONVEX1:def 1;

then consider b being Element of (TOP-REAL n) such that

A22: z = s * b and

A23: 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 A24: |.c.| <= |.(c - y).| + |.y.| by EUCLID:12;

A25: dist (X,e) < m by A23, METRIC_1:11;

then |.(c - y).| < m by SPPOL_1:5;

then |.(c - y).| + |.y.| <= m + |.x.| by XREAL_1:6;

then |.c.| <= m + |.x.| by A24, XXREAL_0:2;

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 COMPLEX1:46, SPPOL_1:5;

then |.((a * y) + (- (a * c))).| <= |.a.| * m by A25, A27, XREAL_1:64;

then A28: |.((a * y) + (- (a * c))).| < r / 2 by A20, 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))).| = |.(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 A21, XCMPLX_1:87, XREAL_1:64;

then |.((a * c) + (- (s * c))).| <= r / 2 by A26, XXREAL_0:2;

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 A28, 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 SPPOL_1:5;

then dist (AX,se) < r by A29, XXREAL_0:2;

then se in Ball (AX,r) by METRIC_1:11;

hence z in V by A16, A22; :: thesis: verum

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;

thus TOP-REAL n is add-continuous :: thesis: TOP-REAL n is Mult-continuous

proof

let a be Real; :: according to RLTOPSP1:def 9 :: thesis: for b
let x1, x2 be Point of (TOP-REAL n); :: according to RLTOPSP1:def 8 :: thesis: for b_{1} being Element of bool the carrier of (TOP-REAL n) holds

( not b_{1} is open or not x1 + x2 in b_{1} or ex b_{2}, b_{3} being Element of bool the carrier of (TOP-REAL n) st

( b_{2} is open & b_{3} is open & x1 in b_{2} & x2 in b_{3} & b_{2} + b_{3} c= b_{1} ) )

let V be Subset of (TOP-REAL n); :: thesis: ( not V is open or not x1 + x2 in V or ex b_{1}, b_{2} being Element of bool the carrier of (TOP-REAL n) st

( b_{1} is open & b_{2} is open & x1 in b_{1} & x2 in b_{2} & b_{1} + b_{2} c= V ) )

assume that

A2: V is open and

A3: x1 + x2 in V ; :: thesis: ex b_{1}, b_{2} being Element of bool the carrier of (TOP-REAL n) st

( b_{1} is open & b_{2} is open & x1 in b_{1} & x2 in b_{2} & b_{1} + b_{2} 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 A2, PRE_TOPC:def 2;

then v is open by A1, PRE_TOPC:def 2;

then consider r being Real such that

A4: r > 0 and

A5: Ball (X12,r) c= v by A3, 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_{1} being Element of bool the carrier of (TOP-REAL n) st

( B1 is open & b_{1} is open & x1 in B1 & x2 in b_{1} & B1 + b_{1} 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 A4, GOBOARD6:1, GOBOARD6:3, XREAL_1:215; :: 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 (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

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 (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 A8, METRIC_1:11;

then A9: |.(y2 - c2).| < r / 2 by SPPOL_1:5;

dist (X1,e1) < r / 2 by A7, METRIC_1:11;

then |.(y1 - c1).| < r / 2 by SPPOL_1:5;

then A10: |.(y1 - c1).| + |.(y2 - c2).| < (r / 2) + (r / 2) by A9, XREAL_1:8;

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 A11, SPPOL_1:5;

|.((y1 - c1) + (y2 - c2)).| <= |.(y1 - c1).| + |.(y2 - c2).| by EUCLID:12;

then dist (X12,e12) < r by A10, A12, XXREAL_0:2;

then e12 in Ball (X12,r) by METRIC_1:11;

hence x in V by A5, A6; :: thesis: verum

end;( not b

( b

let V be Subset of (TOP-REAL n); :: thesis: ( not V is open or not x1 + x2 in V or ex b

( b

assume that

A2: V is open and

A3: x1 + x2 in V ; :: thesis: ex b

( b

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 A2, PRE_TOPC:def 2;

then v is open by A1, PRE_TOPC:def 2;

then consider r being Real such that

A4: r > 0 and

A5: Ball (X12,r) c= v by A3, 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

( B1 is open & b

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 A4, GOBOARD6:1, GOBOARD6:3, XREAL_1:215; :: 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 (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

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 (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 A8, METRIC_1:11;

then A9: |.(y2 - c2).| < r / 2 by SPPOL_1:5;

dist (X1,e1) < r / 2 by A7, METRIC_1:11;

then |.(y1 - c1).| < r / 2 by SPPOL_1:5;

then A10: |.(y1 - c1).| + |.(y2 - c2).| < (r / 2) + (r / 2) by A9, XREAL_1:8;

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 A11, SPPOL_1:5;

|.((y1 - c1) + (y2 - c2)).| <= |.(y1 - c1).| + |.(y2 - c2).| by EUCLID:12;

then dist (X12,e12) < r by A10, A12, XXREAL_0:2;

then e12 in Ball (X12,r) by METRIC_1:11;

hence x in V by A5, A6; :: thesis: verum

for b

( not b

( b

( b

let x be Point of (TOP-REAL n); :: thesis: for b

( not b

( b

( b

let V be Subset of (TOP-REAL n); :: thesis: ( not V is open or not a * x in V or ex b

( b

( b

assume that

A13: V is open and

A14: a * x in V ; :: thesis: ex b

( b

( b

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 A13, PRE_TOPC:def 2;

then v is open by A1, PRE_TOPC:def 2;

then consider r being Real such that

A15: r > 0 and

A16: Ball (AX,r) c= v by A14, TOPMETR:15;

set r2 = r / 2;

A17: r / 2 > 0 by A15, XREAL_1:215;

then A18: (r / 2) / 2 > 0 by XREAL_1:215;

ex m being positive Real st |.a.| * m < r / 2

proof
end;

then consider m being positive Real such that per cases
( |.a.| = 0 or |.a.| > 0 )
by COMPLEX1:46;

end;

suppose
|.a.| = 0
; :: thesis: ex m being positive Real st |.a.| * m < r / 2

then
|.a.| * 1 < r / 2
by A15, XREAL_1:215;

hence ex m being positive Real st |.a.| * m < r / 2 ; :: thesis: verum

end;hence ex m being positive Real st |.a.| * m < r / 2 ; :: thesis: verum

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 A18, XREAL_1:139;

take m ; :: thesis: |.a.| * m < r / 2

(r / 2) / 2 < r / 2 by A15, XREAL_1:215, XREAL_1:216;

hence |.a.| * m < r / 2 by A19, XCMPLX_1:87; :: thesis: verum

end;take m ; :: thesis: |.a.| * m < r / 2

(r / 2) / 2 < r / 2 by A15, XREAL_1:215, XREAL_1:216;

hence |.a.| * m < r / 2 by A19, XCMPLX_1:87; :: thesis: verum

A20: |.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 A17, XREAL_1:139;

take nr ; :: thesis: ex b

( b

( nr <= |.(b

take B ; :: thesis: ( B is open & x in B & ( for b

( nr <= |.(b

thus ( B is open & x in B ) by GOBOARD6:1, GOBOARD6:3; :: thesis: for b

( nr <= |.(b

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 (TOP-REAL n) : b in B } by CONVEX1:def 1;

then consider b being Element of (TOP-REAL n) such that

A22: z = s * b and

A23: 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 A24: |.c.| <= |.(c - y).| + |.y.| by EUCLID:12;

A25: dist (X,e) < m by A23, METRIC_1:11;

then |.(c - y).| < m by SPPOL_1:5;

then |.(c - y).| + |.y.| <= m + |.x.| by XREAL_1:6;

then |.c.| <= m + |.x.| by A24, XXREAL_0:2;

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 COMPLEX1:46, SPPOL_1:5;

then |.((a * y) + (- (a * c))).| <= |.a.| * m by A25, A27, XREAL_1:64;

then A28: |.((a * y) + (- (a * c))).| < r / 2 by A20, 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))).| = |.(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 A21, XCMPLX_1:87, XREAL_1:64;

then |.((a * c) + (- (s * c))).| <= r / 2 by A26, XXREAL_0:2;

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 A28, 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 SPPOL_1:5;

then dist (AX,se) < r by A29, XXREAL_0:2;

then se in Ball (AX,r) by METRIC_1:11;

hence z in V by A16, A22; :: thesis: verum