let n be Element of NAT ; :: thesis: for F being Function of [:(TOP-REAL n),I[01] :],(TOP-REAL n) st ( for x being Point of (TOP-REAL n)
for i being Point of I[01] holds F . x,i = i * x ) holds
F is continuous
let F be Function of [:(TOP-REAL n),I[01] :],(TOP-REAL n); :: thesis: ( ( for x being Point of (TOP-REAL n)
for i being Point of I[01] holds F . x,i = i * x ) implies F is continuous )
assume A1: for x being Point of (TOP-REAL n)
for i being Point of I[01] holds F . x,i = i * x ; :: thesis: F is continuous
set I = the carrier of I[01] ;
A2: [#] I[01] = the carrier of I[01] ;
A3: REAL n = n -tuples_on REAL by EUCLID:def 1;
for p being Point of [:(TOP-REAL n),I[01] :]
for V being Subset of (TOP-REAL n) st F . p in V & V is open holds
ex W being Subset of [:(TOP-REAL n),I[01] :] st
( p in W & W is open & F .: W c= V )

proof

let p be Point of [:(TOP-REAL n),I[01] :]; :: thesis: for V being Subset of (TOP-REAL n) st F . p in V & V is open holds
ex W being Subset of [:(TOP-REAL n),I[01] :] st
( p in W & W is open & F .: W c= V )
let V be Subset of (TOP-REAL n); :: thesis: ( F . p in V & V is open implies ex W being Subset of [:(TOP-REAL n),I[01] :] st
( p in W & W is open & F .: W c= V ) )
assume ( F . p in V & V is open ) ; :: thesis: ex W being Subset of [:(TOP-REAL n),I[01] :] st
( p in W & W is open & F .: W c= V )
then A4: F . p in Int V by TOPS_1:55;
reconsider ep = F . p as Point of (Euclid n) by TOPREAL3:13;
consider x being Point of (TOP-REAL n), i being Point of I[01] such that
A5: p = [x,i] by BORSUK_1:50;
consider r0 being real number such that
A6: r0 > 0 and
A7: Ball ep,r0 c= V by A4, GOBOARD6:8;
reconsider lx = x as Point of (Euclid n) by TOPREAL3:13;
reconsider fx = x as Element of REAL n by EUCLID:25;
A8: r0 / 2 > 0 by A6, XREAL_1:141;
A9: ep = F . x,i by A5
.= i * x by A1 ;

per cases ( i > 0 or i <= 0 ) ;

suppose A10: i > 0 ; :: thesis: ex W being Subset of [:(TOP-REAL n),I[01] :] st
( p in W & W is open & F .: W c= V )

reconsider B = Ball lx,((r0 / 2) / i) as Subset of (TOP-REAL n) by TOPREAL3:13;
set t = ((2 * i) * |.fx.|) + r0;
set c = (i * r0) / (((2 * i) * |.fx.|) + r0);
set X1 = ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[;
set X2 = ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[ /\ the carrier of I[01] ;
A11: 0 < 2 * i by A10, XREAL_1:131;
then 0 <= (2 * i) * |.fx.| ;
then A13: 0 + 0 < ((2 * i) * |.fx.|) + r0 by A6;
0 < i * r0 by A6, A10, XREAL_1:131;
then A14: 0 < (i * r0) / (((2 * i) * |.fx.|) + r0) by A13, XREAL_1:141;
reconsider X2 = ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[ /\ the carrier of I[01] as Subset of I[01] by XBOOLE_1:17;
take W = [:B,X2:]; :: thesis: ( p in W & W is open & F .: W c= V )
A15: x in B by A8, A10, GOBOARD6:4, XREAL_1:141;
abs (i - i) < (i * r0) / (((2 * i) * |.fx.|) + r0) by A14, ABSVALUE:def 1;
then i in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[ by RCOMP_1:8;
then i in X2 by XBOOLE_0:def 4;
hence p in W by A5, A15, ZFMISC_1:106; :: thesis: ( W is open & F .: W c= V )
A16: 0 <= i * ((2 * i) * |.fx.|) by A10;
A17: i - ((i * r0) / (((2 * i) * |.fx.|) + r0)) = ((i * (((2 * i) * |.fx.|) + r0)) / (((2 * i) * |.fx.|) + r0)) - ((i * r0) / (((2 * i) * |.fx.|) + r0)) by A13, XCMPLX_1:90
.= ((i * (((2 * i) * |.fx.|) + r0)) - (i * r0)) / (((2 * i) * |.fx.|) + r0) by XCMPLX_1:121
.= (i * ((2 * i) * |.fx.|)) / (((2 * i) * |.fx.|) + r0) ;
then A18: 0 <= i - ((i * r0) / (((2 * i) * |.fx.|) + r0)) by A13, A16;
A19: (i - ((i * r0) / (((2 * i) * |.fx.|) + r0))) - 1 = ((i * ((2 * i) * |.fx.|)) / (((2 * i) * |.fx.|) + r0)) - ((((2 * i) * |.fx.|) + r0) / (((2 * i) * |.fx.|) + r0)) by A13, A17, XCMPLX_1:60
.= ((i * ((2 * i) * |.fx.|)) - (((2 * i) * |.fx.|) + r0)) / (((2 * i) * |.fx.|) + r0) by XCMPLX_1:121 ;
i <= 1 by BORSUK_1:86;
then 1 - 1 >= i - 1 by XREAL_1:11;
then ((2 * i) * |.fx.|) * (i - 1) <= 0 by A11;
then ((i * ((2 * i) * |.fx.|)) - ((2 * i) * |.fx.|)) - r0 < r0 - r0 by A6;
then (i - ((i * r0) / (((2 * i) * |.fx.|) + r0))) - 1 < 0 by A13, A19, XREAL_1:143;
then ((i - ((i * r0) / (((2 * i) * |.fx.|) + r0))) - 1) + 1 < 0 + 1 by XREAL_1:10;
then A20: i - ((i * r0) / (((2 * i) * |.fx.|) + r0)) is Point of I[01] by A18, BORSUK_1:86;

A21: now

per cases ( i + ((i * r0) / (((2 * i) * |.fx.|) + r0)) <= 1 or i + ((i * r0) / (((2 * i) * |.fx.|) + r0)) > 1 ) ;

suppose A22: i + ((i * r0) / (((2 * i) * |.fx.|) + r0)) <= 1 ; :: thesis: X2 is open

].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[ c= the carrier of I[01]

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[ or a in the carrier of I[01] )
assume A23: a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[ ; :: thesis: a in the carrier of I[01]
then reconsider a = a as Real ;
( i - ((i * r0) / (((2 * i) * |.fx.|) + r0)) < a & a < i + ((i * r0) / (((2 * i) * |.fx.|) + r0)) ) by A23, XXREAL_1:4;
then ( 0 < a & a < 1 ) by A13, A16, A17, A22, XXREAL_0:2;
hence a in the carrier of I[01] by BORSUK_1:86; :: thesis: verum

end;

then reconsider X1 = ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[ as Subset of I[01] ;
0 + 0 <= i + ((i * r0) / (((2 * i) * |.fx.|) + r0)) by A10, A14;
then i + ((i * r0) / (((2 * i) * |.fx.|) + r0)) is Point of I[01] by A22, BORSUK_1:86;
then X1 is open by A20, BORSUK_4:70;
hence X2 is open by A2, TOPS_1:38; :: thesis: verum

end;

suppose A24: i + ((i * r0) / (((2 * i) * |.fx.|) + r0)) > 1 ; :: thesis: X2 is open

X2 = ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),1.]

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),1.] c= X2

let a be set ; :: thesis: ( a in X2 implies a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),1.] )
assume A25: a in X2 ; :: thesis: a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),1.]
then A26: a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[ by XBOOLE_0:def 4;
reconsider b = a as Real by A25;
A27: i - ((i * r0) / (((2 * i) * |.fx.|) + r0)) < b by A26, XXREAL_1:4;
b <= 1 by A25, BORSUK_1:86;
hence a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),1.] by A27, XXREAL_1:2; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),1.] or a in X2 )
assume A28: a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),1.] ; :: thesis: a in X2
then reconsider b = a as Real ;
A29: i - ((i * r0) / (((2 * i) * |.fx.|) + r0)) < b by A28, XXREAL_1:2;
A30: b <= 1 by A28, XXREAL_1:2;
then b < i + ((i * r0) / (((2 * i) * |.fx.|) + r0)) by A24, XXREAL_0:2;
then A31: a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[ by A29, XXREAL_1:4;
a in the carrier of I[01] by A18, A29, A30, BORSUK_1:83, XXREAL_1:1;
hence a in X2 by A31, XBOOLE_0:def 4; :: thesis: verum

end;

hence X2 is open by A20, Th4; :: thesis: verum

end;

end;

end;

B is open by GOBOARD6:6;
hence W is open by A21, BORSUK_1:46; :: thesis: F .: W c= V
F .: W c= Ball ep,r0

proof

let m be set ; :: according to TARSKI:def 3 :: thesis: ( not m in F .: W or m in Ball ep,r0 )
assume m in F .: W ; :: thesis: m in Ball ep,r0
then consider z being set such that
A32: z in dom F and
A33: z in W and
A34: F . z = m by FUNCT_1:def 12;
reconsider z = z as Point of [:(TOP-REAL n),I[01] :] by A32;
consider y being Point of (TOP-REAL n), j being Point of I[01] such that
A35: z = [y,j] by BORSUK_1:50;
reconsider ez = F . z, ey = y as Point of (Euclid n) by TOPREAL3:13;
A36: ez = F . y,j by A35
.= j * y by A1 ;
reconsider fp = ep, fz = ez, fe = i * y, fy = y as Element of REAL n by EUCLID:25;
A37: dist ep,ez = |.(fp - fz).| by SPPOL_1:20;
A38: |.(fp - fz).| <= |.(fp - fe).| + |.(fe - fz).| by EUCLID:22;
fy in B by A33, A35, ZFMISC_1:106;
then A39: dist lx,ey < (r0 / 2) / i by METRIC_1:12;
A40: dist lx,ey = |.(fx - fy).| by SPPOL_1:20;
then A41: i * |.(fx - fy).| < i * ((r0 / 2) / i) by A10, A39, XREAL_1:70;
A42: i * ((r0 / i) / 2) = r0 / 2 by A10, XCMPLX_1:98;
reconsider yy = ey as Element of n -tuples_on REAL by A3, EUCLID:25;
X: ( fe = i * yy & fz = j * yy ) by A3, A38, EUCLID:69, A36;
then Y: fe - fz = (i * yy) - (j * yy) by A3, A38, EUCLID:73;
then A43: |.(fe - fz).| = |.((i - j) * fy).| by A3, A38, Th8
.= (abs (i - j)) * |.fy.| by EUCLID:14 ;
j in X2 by A33, A35, ZFMISC_1:106;
then j in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[ by XBOOLE_0:def 4;
then abs (j - i) < (i * r0) / (((2 * i) * |.fx.|) + r0) by RCOMP_1:8;
then abs (i - j) < (i * r0) / (((2 * i) * |.fx.|) + r0) by UNIFORM1:13;
then A44: (abs (i - j)) * |.fy.| <= ((i * r0) / (((2 * i) * |.fx.|) + r0)) * |.fy.| by XREAL_1:66;
A45: |.(fx - fy).| = |.(fy - fx).| by EUCLID:21;
|.fy.| - |.fx.| <= |.(fy - fx).| by EUCLID:18;
then |.fy.| - |.fx.| < (r0 / 2) / i by A39, A40, A45, XXREAL_0:2;
then |.fy.| < |.fx.| + ((r0 / 2) / i) by XREAL_1:21;
then A46: ((i * r0) / (((2 * i) * |.fx.|) + r0)) * |.fy.| < ((i * r0) / (((2 * i) * |.fx.|) + r0)) * (|.fx.| + ((r0 / 2) / i)) by A14, XREAL_1:70;
((i * r0) / (((2 * i) * |.fx.|) + r0)) * (|.fx.| + ((r0 / 2) / i)) = ((i * r0) / (((2 * i) * |.fx.|) + r0)) * (|.fx.| + (r0 / (2 * i))) by XCMPLX_1:79
.= ((i * r0) / (((2 * i) * |.fx.|) + r0)) * (((|.fx.| * (2 * i)) / (2 * i)) + (r0 / (2 * i))) by A11, XCMPLX_1:90
.= ((i * r0) / (((2 * i) * |.fx.|) + r0)) * (((|.fx.| * (2 * i)) + r0) / (2 * i)) by XCMPLX_1:63
.= (i * r0) / (2 * i) by A13, XCMPLX_1:99
.= r0 / 2 by A10, XCMPLX_1:92 ;
then A47: (abs (i - j)) * |.fy.| <= r0 / 2 by A44, A46, XXREAL_0:2;
reconsider yy = y as Element of n -tuples_on REAL by A3, EUCLID:25;
fe = i * yy by EUCLID:69, X;
then U: (i * fx) - fe = (i * fx) - (i * yy) by EUCLID:73
.= i * (fx - fy) by A3, Th7 ;
fp = i * fx by A9, A43, A47, EUCLID:69;
then UU: (i * fx) - fe = fp - fe by A9, A43, A47;
V: |.(fe - fz).| = |.((i * yy) - (j * yy)).| by Y
.= |.((i - j) * yy).| by Th7, Th8
.= |.((i - j) * fy).| by EUCLID:69
.= (abs (i - j)) * |.fy.| by EUCLID:14
.= (abs (i - j)) * |.fy.| by A10, A41, A42, ABSVALUE:def 1 ;
(r0 / 2) / i = (r0 / i) / 2 by XCMPLX_1:48;
then (abs i) * |.(fx - fy).| < r0 / 2 by A10, A41, A42, ABSVALUE:def 1;
then |.(i * (fx - fy)).| < r0 / 2 by EUCLID:14;
then |.((i * fx) - fe).| < r0 / 2 by A3, Th7, U;
then |.(fp - fe).| + |.(fe - fz).| < (r0 / 2) + (r0 / 2) by A9, A43, A47, XREAL_1:10, UU, V;
then dist ep,ez < r0 by A37, A38, XXREAL_0:2;
hence m in Ball ep,r0 by A34, METRIC_1:12; :: thesis: verum

end;

hence F .: W c= V by A7, XBOOLE_1:1; :: thesis: verum

end;

suppose i <= 0 ; :: thesis: ex W being Subset of [:(TOP-REAL n),I[01] :] st
( p in W & W is open & F .: W c= V )

then A48: i = 0 by BORSUK_1:86;
A49: r0 is Real by XREAL_0:def 1;
reconsider B = Ball lx,r0 as Subset of (TOP-REAL n) by TOPREAL3:13;
set t = |.fx.| + r0;
set c = r0 / (|.fx.| + r0);
set X1 = [.0 ,(r0 / (|.fx.| + r0)).[;
A50: 0 < r0 / (|.fx.| + r0) by A6, XREAL_1:141;
0 + r0 <= |.fx.| + r0 by XREAL_1:9;
then A51: r0 / (|.fx.| + r0) <= 1 by A6, XREAL_1:187;
then A52: r0 / (|.fx.| + r0) is Point of I[01] by A50, BORSUK_1:86;
[.0 ,(r0 / (|.fx.| + r0)).[ c= the carrier of I[01]

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in [.0 ,(r0 / (|.fx.| + r0)).[ or s in the carrier of I[01] )
assume A53: s in [.0 ,(r0 / (|.fx.| + r0)).[ ; :: thesis: s in the carrier of I[01]
then reconsider s = s as Real ;
A54: 0 <= s by A53, XXREAL_1:3;
s < r0 / (|.fx.| + r0) by A53, XXREAL_1:3;
then s <= 1 by A51, XXREAL_0:2;
hence s in the carrier of I[01] by A54, BORSUK_1:86; :: thesis: verum

end;

then reconsider X1 = [.0 ,(r0 / (|.fx.| + r0)).[ as Subset of I[01] ;
take W = [:B,X1:]; :: thesis: ( p in W & W is open & F .: W c= V )
A55: x in B by A6, GOBOARD6:4;
i in X1 by A48, A50, XXREAL_1:3;
hence p in W by A5, A55, ZFMISC_1:106; :: thesis: ( W is open & F .: W c= V )
A56: X1 is open by A52, Th5;
B is open by A49, GOBOARD6:6;
hence W is open by A56, BORSUK_1:46; :: thesis: F .: W c= V
F .: W c= Ball ep,r0

proof

let m be set ; :: according to TARSKI:def 3 :: thesis: ( not m in F .: W or m in Ball ep,r0 )
assume m in F .: W ; :: thesis: m in Ball ep,r0
then consider z being set such that
A57: z in dom F and
A58: z in W and
A59: F . z = m by FUNCT_1:def 12;
reconsider z = z as Point of [:(TOP-REAL n),I[01] :] by A57;
consider y being Point of (TOP-REAL n), j being Point of I[01] such that
A60: z = [y,j] by BORSUK_1:50;
reconsider ez = F . z, ey = y as Point of (Euclid n) by TOPREAL3:13;
A61: ez = F . y,j by A60
.= j * y by A1 ;
reconsider fp = ep, fz = ez, fy = y as Element of REAL n by EUCLID:25;
A62: (F . z) - (0. (TOP-REAL n)) = F . z by RLVECT_1:26, RLVECT_1:27;
A63: 0 <= j by BORSUK_1:86;
X1: fz = F . z ;
fp = i * x by A9
.= 0. (TOP-REAL n) by A62, EUCLID:33, A48 ;
then A64: fz - fp = (F . z) - (0. (TOP-REAL n)) by A62, EUCLID:73
.= fz by A9, A48, A62, EUCLID:33 ;
X2: |.(j * fy).| = (abs j) * |.fy.| by EUCLID:14;
A65: dist ep,ez = |.(fz - fp).| by SPPOL_1:20
.= |.fz.| by A64
.= |.(j * fy).| by A61, A64, EUCLID:69
.= (abs j) * |.fy.| by A61, A64, X2
.= j * |.fy.| by A63, ABSVALUE:def 1 ;
fy in B by A58, A60, ZFMISC_1:106;
then A66: dist lx,ey < r0 by METRIC_1:12;
A67: dist lx,ey = |.(fx - fy).| by SPPOL_1:20;
A68: |.(fx - fy).| = |.(fy - fx).| by EUCLID:21;
|.fy.| - |.fx.| <= |.(fy - fx).| by EUCLID:18;
then |.fy.| - |.fx.| < r0 by A66, A67, A68, XXREAL_0:2;
then A69: |.fy.| < |.fx.| + r0 by XREAL_1:21;

now

per cases ( 0 < j or j <= 0 ) ;

suppose A70: 0 < j ; :: thesis: j * |.fy.| < r0

j in X1 by A58, A60, ZFMISC_1:106;
then j < r0 / (|.fx.| + r0) by XXREAL_1:3;
then r0 / j > r0 / (r0 / (|.fx.| + r0)) by A6, A70, XREAL_1:78;
then |.fx.| + r0 < r0 / j by A50, XCMPLX_1:54;
then |.fy.| < r0 / j by A69, XXREAL_0:2;
then j * |.fy.| < j * (r0 / j) by A70, XREAL_1:70;
hence j * |.fy.| < r0 by A70, XCMPLX_1:88; :: thesis: verum

end;

suppose j <= 0 ; :: thesis: j * |.fy.| < r0

then j = 0 by BORSUK_1:86;
hence j * |.fy.| < r0 by A6; :: thesis: verum

end;

end;

end;

hence m in Ball ep,r0 by A59, A65, METRIC_1:12; :: thesis: verum

end;

hence F .: W c= V by A7, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

hence F is continuous by JGRAPH_2:20; :: thesis: verum