let n be 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
set I = the carrier of I[01];
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
A2: REAL n = n -tuples_on REAL by EUCLID:def 1;
A3: [#] I[01] = the carrier of I[01] ;
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 ) )
reconsider ep = F . p as Point of (Euclid n) by TOPREAL3:8;
consider x being Point of (TOP-REAL n), i being Point of I[01] such that
A4: p = [x,i] by BORSUK_1:10;
A5: ep = F . (x,i) by A4
.= i * x by A1 ;
reconsider fx = x as Element of REAL n by EUCLID:22;
reconsider lx = x as Point of (Euclid n) by TOPREAL3:8;
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 F . p in Int V by TOPS_1:23;
then consider r0 being Real such that
A6: r0 > 0 and
A7: Ball (ep,r0) c= V by GOBOARD6:5;
A8: r0 / 2 > 0 by A6, XREAL_1:139;

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

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

set t = ((2 * i) * |.fx.|) + r0;
set c = (i * r0) / (((2 * i) * |.fx.|) + r0);
i <= 1 by BORSUK_1:43;
then 1 - 1 >= i - 1 by XREAL_1:9;
then ((2 * i) * |.fx.|) * (i - 1) <= 0 by A9;
then A10: ((i * ((2 * i) * |.fx.|)) - ((2 * i) * |.fx.|)) - r0 < r0 - r0 by A6;
A11: i - ((i * r0) / (((2 * i) * |.fx.|) + r0)) = ((i * (((2 * i) * |.fx.|) + r0)) / (((2 * i) * |.fx.|) + r0)) - ((i * r0) / (((2 * i) * |.fx.|) + r0)) by A6, A9, XCMPLX_1:89
.= ((i * (((2 * i) * |.fx.|) + r0)) - (i * r0)) / (((2 * i) * |.fx.|) + r0) by XCMPLX_1:120
.= (i * ((2 * i) * |.fx.|)) / (((2 * i) * |.fx.|) + r0) ;
then (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 A6, A9, XCMPLX_1:60
.= ((i * ((2 * i) * |.fx.|)) - (((2 * i) * |.fx.|) + r0)) / (((2 * i) * |.fx.|) + r0) by XCMPLX_1:120 ;
then (i - ((i * r0) / (((2 * i) * |.fx.|) + r0))) - 1 < 0 by A6, A9, A10, XREAL_1:141;
then ((i - ((i * r0) / (((2 * i) * |.fx.|) + r0))) - 1) + 1 < 0 + 1 by XREAL_1:8;
then A12: i - ((i * r0) / (((2 * i) * |.fx.|) + r0)) is Point of I[01] by A6, A9, A11, BORSUK_1:43;
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];
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;
reconsider B = Ball (lx,((r0 / 2) / i)) as Subset of (TOP-REAL n) by TOPREAL3:8;
take W = [:B,X2:]; :: thesis: ( p in W & W is open & F .: W c= V )
0 < i * r0 by A6, A9, XREAL_1:129;
then A13: 0 < (i * r0) / (((2 * i) * |.fx.|) + r0) by A6, A9, XREAL_1:139;
then |.(i - i).| < (i * r0) / (((2 * i) * |.fx.|) + r0) by ABSVALUE:def 1;
then i in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[ by RCOMP_1:1;
then A14: i in X2 by XBOOLE_0:def 4;
A15: 0 <= i - ((i * r0) / (((2 * i) * |.fx.|) + r0)) by A6, A9, A11;

A16: now :: thesis: X2 is open

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

suppose A17: 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 object ; :: 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 A18: 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 ;
a < i + ((i * r0) / (((2 * i) * |.fx.|) + r0)) by A18, XXREAL_1:4;
then A19: a < 1 by A17, XXREAL_0:2;
0 < a by A6, A9, A11, A18, XXREAL_1:4;
hence a in the carrier of I[01] by A19, BORSUK_1:43; :: 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] ;
i + ((i * r0) / (((2 * i) * |.fx.|) + r0)) is Point of I[01] by A6, A9, A17, BORSUK_1:43;
then X1 is open by A12, BORSUK_4:45;
hence X2 is open by A3; :: thesis: verum

end;

suppose A20: 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 object ; :: thesis: ( a in X2 implies a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),1.] )
assume A21: a in X2 ; :: thesis: a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),1.]
then reconsider b = a as Real ;
a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[ by A21, XBOOLE_0:def 4;
then A22: i - ((i * r0) / (((2 * i) * |.fx.|) + r0)) < b by XXREAL_1:4;
b <= 1 by A21, BORSUK_1:43;
hence a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),1.] by A22, XXREAL_1:2; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),1.] or a in X2 )
assume A23: a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),1.] ; :: thesis: a in X2
then reconsider b = a as Real ;
A24: i - ((i * r0) / (((2 * i) * |.fx.|) + r0)) < b by A23, XXREAL_1:2;
A25: b <= 1 by A23, XXREAL_1:2;
then b < i + ((i * r0) / (((2 * i) * |.fx.|) + r0)) by A20, XXREAL_0:2;
then A26: a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[ by A24, XXREAL_1:4;
a in the carrier of I[01] by A15, A24, A25, BORSUK_1:40, XXREAL_1:1;
hence a in X2 by A26, XBOOLE_0:def 4; :: thesis: verum

end;

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

end;

end;

end;

x in B by A8, A9, GOBOARD6:1, XREAL_1:139;
hence p in W by A4, A14, ZFMISC_1:87; :: thesis: ( W is open & F .: W c= V )
B is open by GOBOARD6:3;
hence W is open by A16, BORSUK_1:6; :: thesis: F .: W c= V
A27: 0 < 2 * i by A9, XREAL_1:129;
F .: W c= Ball (ep,r0)

proof

let m be object ; :: 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 object such that
A28: z in dom F and
A29: z in W and
A30: F . z = m by FUNCT_1:def 6;
reconsider z = z as Point of [:(TOP-REAL n),I[01]:] by A28;
consider y being Point of (TOP-REAL n), j being Point of I[01] such that
A31: z = [y,j] by BORSUK_1:10;
reconsider ez = F . z, ey = y as Point of (Euclid n) by TOPREAL3:8;
reconsider fp = ep, fz = ez, fe = i * y, fy = y as Element of REAL n by EUCLID:22;
A32: ( i * ((r0 / i) / 2) = r0 / 2 & (r0 / 2) / i = (r0 / i) / 2 ) by A9, XCMPLX_1:48, XCMPLX_1:97;
fy in B by A29, A31, ZFMISC_1:87;
then A33: dist (lx,ey) < (r0 / 2) / i by METRIC_1:11;
j in X2 by A29, A31, ZFMISC_1:87;
then j in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[ by XBOOLE_0:def 4;
then |.(j - i).| < (i * r0) / (((2 * i) * |.fx.|) + r0) by RCOMP_1:1;
then |.(i - j).| < (i * r0) / (((2 * i) * |.fx.|) + r0) by UNIFORM1:11;
then A34: |.(i - j).| * |.fy.| <= ((i * r0) / (((2 * i) * |.fx.|) + r0)) * |.fy.| by XREAL_1:64;
reconsider yy = ey as Element of n -tuples_on REAL by A2, EUCLID:22;
ez = F . (y,j) by A31
.= j * y by A1 ;
then fe - fz = (i * yy) - (j * yy) ;
then A35: |.(fe - fz).| = |.((i - j) * fy).| by Th8
.= |.(i - j).| * |.fy.| by EUCLID:11 ;
reconsider yy = y as Element of n -tuples_on REAL by A2, EUCLID:22;
A36: ( dist (ep,ez) = |.(fp - fz).| & |.(fp - fz).| <= |.(fp - fe).| + |.(fe - fz).| ) by EUCLID:19, SPPOL_1:5;
A37: dist (lx,ey) = |.(fx - fy).| by SPPOL_1:5;
then i * |.(fx - fy).| < i * ((r0 / 2) / i) by A9, A33, XREAL_1:68;
then A38: |.i.| * |.(fx - fy).| < r0 / 2 by A9, A32, ABSVALUE:def 1;
( |.(fx - fy).| = |.(fy - fx).| & |.fy.| - |.fx.| <= |.(fy - fx).| ) by EUCLID:15, EUCLID:18;
then |.fy.| - |.fx.| < (r0 / 2) / i by A33, A37, XXREAL_0:2;
then |.fy.| < |.fx.| + ((r0 / 2) / i) by XREAL_1:19;
then A39: ((i * r0) / (((2 * i) * |.fx.|) + r0)) * |.fy.| < ((i * r0) / (((2 * i) * |.fx.|) + r0)) * (|.fx.| + ((r0 / 2) / i)) by A13, XREAL_1:68;
((i * r0) / (((2 * i) * |.fx.|) + r0)) * (|.fx.| + ((r0 / 2) / i)) = ((i * r0) / (((2 * i) * |.fx.|) + r0)) * (|.fx.| + (r0 / (2 * i))) by XCMPLX_1:78
.= ((i * r0) / (((2 * i) * |.fx.|) + r0)) * (((|.fx.| * (2 * i)) / (2 * i)) + (r0 / (2 * i))) by A27, XCMPLX_1:89
.= ((i * r0) / (((2 * i) * |.fx.|) + r0)) * (((|.fx.| * (2 * i)) + r0) / (2 * i)) by XCMPLX_1:62
.= (i * r0) / (2 * i) by A6, A9, XCMPLX_1:98
.= r0 / 2 by A9, XCMPLX_1:91 ;
then A40: |.(i - j).| * |.fy.| <= r0 / 2 by A34, A39, XXREAL_0:2;
(i * fx) - fe = (i * fx) - (i * yy)
.= i * (fx - fy) by Th7 ;
then A41: |.((i * fx) - fe).| < r0 / 2 by A38, EUCLID:11;
(i * fx) - fe = fp - fe by A5;
then |.(fp - fe).| + |.(fe - fz).| < (r0 / 2) + (r0 / 2) by A35, A40, A41, XREAL_1:8;
then dist (ep,ez) < r0 by A36, XXREAL_0:2;
hence m in Ball (ep,r0) by A30, METRIC_1:11; :: thesis: verum

end;

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

end;

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

set t = |.fx.| + r0;
reconsider B = Ball (lx,r0) as Subset of (TOP-REAL n) by TOPREAL3:8;
set c = r0 / (|.fx.| + r0);
set X1 = [.0,(r0 / (|.fx.| + r0)).[;
A43: 0 < r0 / (|.fx.| + r0) by A6, XREAL_1:139;
0 + r0 <= |.fx.| + r0 by XREAL_1:7;
then A44: r0 / (|.fx.| + r0) <= 1 by A6, XREAL_1:185;
A45: [.0,(r0 / (|.fx.| + r0)).[ c= the carrier of I[01]

proof

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

end;

A48: B is open by GOBOARD6:3;
reconsider X1 = [.0,(r0 / (|.fx.| + r0)).[ as Subset of I[01] by A45;
take W = [:B,X1:]; :: thesis: ( p in W & W is open & F .: W c= V )
A49: x in B by A6, GOBOARD6:1;
A50: i = 0 by A42, BORSUK_1:43;
then i in X1 by A43, XXREAL_1:3;
hence p in W by A4, A49, ZFMISC_1:87; :: thesis: ( W is open & F .: W c= V )
r0 / (|.fx.| + r0) is Point of I[01] by A6, A44, BORSUK_1:43;
then X1 is open by Th5;
hence W is open by A48, BORSUK_1:6; :: thesis: F .: W c= V
F .: W c= Ball (ep,r0)

proof

let m be object ; :: 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 object such that
A51: z in dom F and
A52: z in W and
A53: F . z = m by FUNCT_1:def 6;
reconsider z = z as Point of [:(TOP-REAL n),I[01]:] by A51;
consider y being Point of (TOP-REAL n), j being Point of I[01] such that
A54: z = [y,j] by BORSUK_1:10;
reconsider ez = F . z, ey = y as Point of (Euclid n) by TOPREAL3:8;
reconsider fp = ep, fz = ez, fy = y as Element of REAL n by EUCLID:22;
fy in B by A52, A54, ZFMISC_1:87;
then A55: dist (lx,ey) < r0 by METRIC_1:11;
A56: ez = F . (y,j) by A54
.= j * y by A1 ;
fp = i * x by A5
.= 0. (TOP-REAL n) by A50, RLVECT_1:10 ;
then A57: fz - fp = (F . z) - (0. (TOP-REAL n))
.= fz by RLVECT_1:13 ;
A58: |.fy.| - |.fx.| <= |.(fy - fx).| by EUCLID:15;
( dist (lx,ey) = |.(fx - fy).| & |.(fx - fy).| = |.(fy - fx).| ) by EUCLID:18, SPPOL_1:5;
then |.fy.| - |.fx.| < r0 by A55, A58, XXREAL_0:2;
then A59: |.fy.| < |.fx.| + r0 by XREAL_1:19;

A60: now :: thesis: j * |.fy.| < r0

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

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

j in X1 by A52, A54, ZFMISC_1:87;
then j < r0 / (|.fx.| + r0) by XXREAL_1:3;
then r0 / j > r0 / (r0 / (|.fx.| + r0)) by A6, A61, XREAL_1:76;
then |.fx.| + r0 < r0 / j by A43, XCMPLX_1:54;
then |.fy.| < r0 / j by A59, XXREAL_0:2;
then j * |.fy.| < j * (r0 / j) by A61, XREAL_1:68;
hence j * |.fy.| < r0 by A61, XCMPLX_1:87; :: thesis: verum

end;

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

hence j * |.fy.| < r0 by A6; :: thesis: verum

end;

end;

end;

A62: 0 <= j by BORSUK_1:43;
dist (ep,ez) = |.(fz - fp).| by SPPOL_1:5
.= |.fz.| by A57
.= |.(j * fy).| by A56
.= |.j.| * |.fy.| by EUCLID:11
.= j * |.fy.| by A62, ABSVALUE:def 1 ;
hence m in Ball (ep,r0) by A53, A60, METRIC_1:11; :: thesis: verum

end;

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

end;

end;

end;

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