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:13;
consider x being Point of (TOP-REAL n), i being Point of I[01] such that
A4: p = [x,i] by BORSUK_1:50;
A5: ep = F . (x,i) by A4
.= i * x by A1 ;
reconsider fx = x as Element of REAL n by EUCLID:25;
reconsider lx = x as Point of (Euclid n) by TOPREAL3:13;
A6: n in NAT by ORDINAL1:def 13;
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:55;
then consider r0 being real number such that
A7: r0 > 0 and
A8: Ball (ep,r0) c= V by A6, GOBOARD6:8;
A9: r0 / 2 > 0 by A7, XREAL_1:141;

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 )

set t = ((2 * i) * |.fx.|) + r0;
set c = (i * r0) / (((2 * i) * |.fx.|) + r0);
i <= 1 by BORSUK_1:86;
then 1 - 1 >= i - 1 by XREAL_1:11;
then ((2 * i) * |.fx.|) * (i - 1) <= 0 by A10;
then A11: ((i * ((2 * i) * |.fx.|)) - ((2 * i) * |.fx.|)) - r0 < r0 - r0 by A7;
A12: i - ((i * r0) / (((2 * i) * |.fx.|) + r0)) = ((i * (((2 * i) * |.fx.|) + r0)) / (((2 * i) * |.fx.|) + r0)) - ((i * r0) / (((2 * i) * |.fx.|) + r0)) by A7, A10, 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 (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 A7, A10, XCMPLX_1:60
.= ((i * ((2 * i) * |.fx.|)) - (((2 * i) * |.fx.|) + r0)) / (((2 * i) * |.fx.|) + r0) by XCMPLX_1:121 ;
then (i - ((i * r0) / (((2 * i) * |.fx.|) + r0))) - 1 < 0 by A7, A10, A11, XREAL_1:143;
then ((i - ((i * r0) / (((2 * i) * |.fx.|) + r0))) - 1) + 1 < 0 + 1 by XREAL_1:10;
then A13: i - ((i * r0) / (((2 * i) * |.fx.|) + r0)) is Point of I[01] by A7, A10, A12, BORSUK_1:86;
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:13;
take W = [:B,X2:]; :: thesis: ( p in W & W is open & F .: W c= V )
0 < i * r0 by A7, A10, XREAL_1:131;
then A14: 0 < (i * r0) / (((2 * i) * |.fx.|) + r0) by A7, A10, XREAL_1:141;
then abs (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:8;
then A15: i in X2 by XBOOLE_0:def 4;
A16: 0 <= i - ((i * r0) / (((2 * i) * |.fx.|) + r0)) by A7, A10, A12;

A17: now

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

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

end;

suppose A21: 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 A22: 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 A22, XBOOLE_0:def 4;
then A23: i - ((i * r0) / (((2 * i) * |.fx.|) + r0)) < b by XXREAL_1:4;
b <= 1 by A22, BORSUK_1:86;
hence a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),1.] by A23, 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 A24: a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),1.] ; :: thesis: a in X2
then reconsider b = a as Real ;
A25: i - ((i * r0) / (((2 * i) * |.fx.|) + r0)) < b by A24, XXREAL_1:2;
A26: b <= 1 by A24, XXREAL_1:2;
then b < i + ((i * r0) / (((2 * i) * |.fx.|) + r0)) by A21, XXREAL_0:2;
then A27: a in ].(i - ((i * r0) / (((2 * i) * |.fx.|) + r0))),(i + ((i * r0) / (((2 * i) * |.fx.|) + r0))).[ by A25, XXREAL_1:4;
a in the carrier of I[01] by A16, A25, A26, BORSUK_1:83, XXREAL_1:1;
hence a in X2 by A27, XBOOLE_0:def 4; :: thesis: verum

end;

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

end;

end;

end;

x in B by A9, A10, GOBOARD6:4, XREAL_1:141;
hence p in W by A4, A15, ZFMISC_1:106; :: thesis: ( W is open & F .: W c= V )
B is open by A6, GOBOARD6:6;
hence W is open by A17, BORSUK_1:46; :: thesis: F .: W c= V
A28: 0 < 2 * i by A10, XREAL_1:131;
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
A29: z in dom F and
A30: z in W and
A31: F . z = m by FUNCT_1:def 12;
reconsider z = z as Point of [:(TOP-REAL n),I[01]:] by A29;
consider y being Point of (TOP-REAL n), j being Point of I[01] such that
A32: z = [y,j] by BORSUK_1:50;
reconsider ez = F . z, ey = y as Point of (Euclid n) by TOPREAL3:13;
reconsider fp = ep, fz = ez, fe = i * y, fy = y as Element of REAL n by EUCLID:25;
A33: ( i * ((r0 / i) / 2) = r0 / 2 & (r0 / 2) / i = (r0 / i) / 2 ) by A10, XCMPLX_1:48, XCMPLX_1:98;
fy in B by A30, A32, ZFMISC_1:106;
then A34: dist (lx,ey) < (r0 / 2) / i by METRIC_1:12;
j in X2 by A30, A32, 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 A35: (abs (i - j)) * |.fy.| <= ((i * r0) / (((2 * i) * |.fx.|) + r0)) * |.fy.| by XREAL_1:66;
reconsider yy = ey as Element of n -tuples_on REAL by A2, EUCLID:25;
A36: fe = i * yy by EUCLID:69;
ez = F . (y,j) by A32
.= j * y by A1 ;
then fe - fz = (i * yy) - (j * yy) by A36, EUCLID:69;
then A37: |.(fe - fz).| = |.((i - j) * fy).| by Th8
.= (abs (i - j)) * |.fy.| by EUCLID:14 ;
reconsider yy = y as Element of n -tuples_on REAL by A2, EUCLID:25;
A38: ( dist (ep,ez) = |.(fp - fz).| & |.(fp - fz).| <= |.(fp - fe).| + |.(fe - fz).| ) by A6, EUCLID:22, SPPOL_1:20;
A39: dist (lx,ey) = |.(fx - fy).| by A6, SPPOL_1:20;
then i * |.(fx - fy).| < i * ((r0 / 2) / i) by A10, A34, XREAL_1:70;
then A40: (abs i) * |.(fx - fy).| < r0 / 2 by A10, A33, ABSVALUE:def 1;
( |.(fx - fy).| = |.(fy - fx).| & |.fy.| - |.fx.| <= |.(fy - fx).| ) by EUCLID:18, EUCLID:21;
then |.fy.| - |.fx.| < (r0 / 2) / i by A34, A39, XXREAL_0:2;
then |.fy.| < |.fx.| + ((r0 / 2) / i) by XREAL_1:21;
then A41: ((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 A28, XCMPLX_1:90
.= ((i * r0) / (((2 * i) * |.fx.|) + r0)) * (((|.fx.| * (2 * i)) + r0) / (2 * i)) by XCMPLX_1:63
.= (i * r0) / (2 * i) by A7, A10, XCMPLX_1:99
.= r0 / 2 by A10, XCMPLX_1:92 ;
then A42: (abs (i - j)) * |.fy.| <= r0 / 2 by A35, A41, XXREAL_0:2;
(i * fx) - fe = (i * fx) - (i * yy) by EUCLID:69
.= i * (fx - fy) by Th7 ;
then A43: |.((i * fx) - fe).| < r0 / 2 by A40, EUCLID:14;
(i * fx) - fe = fp - fe by A5, EUCLID:69;
then |.(fp - fe).| + |.(fe - fz).| < (r0 / 2) + (r0 / 2) by A37, A42, A43, XREAL_1:10;
then dist (ep,ez) < r0 by A38, XXREAL_0:2;
hence m in Ball (ep,r0) by A31, METRIC_1:12; :: thesis: verum

end;

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

end;

suppose A44: 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:13;
set c = r0 / (|.fx.| + r0);
set X1 = [.0,(r0 / (|.fx.| + r0)).[;
A45: 0 < r0 / (|.fx.| + r0) by A7, XREAL_1:141;
0 + r0 <= |.fx.| + r0 by XREAL_1:9;
then A46: r0 / (|.fx.| + r0) <= 1 by A7, XREAL_1:187;
A47: [.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 A48: 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 A48, XXREAL_1:3;
then A49: s <= 1 by A46, XXREAL_0:2;
0 <= s by A48, XXREAL_1:3;
hence s in the carrier of I[01] by A49, BORSUK_1:86; :: thesis: verum

end;

r0 is Real by XREAL_0:def 1;
then A50: B is open by A6, GOBOARD6:6;
reconsider X1 = [.0,(r0 / (|.fx.| + r0)).[ as Subset of I[01] by A47;
take W = [:B,X1:]; :: thesis: ( p in W & W is open & F .: W c= V )
A51: x in B by A7, GOBOARD6:4;
A52: i = 0 by A44, BORSUK_1:86;
then i in X1 by A45, XXREAL_1:3;
hence p in W by A4, A51, ZFMISC_1:106; :: thesis: ( W is open & F .: W c= V )
r0 / (|.fx.| + r0) is Point of I[01] by A7, A46, BORSUK_1:86;
then X1 is open by Th5;
hence W is open by A50, 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
A53: z in dom F and
A54: z in W and
A55: F . z = m by FUNCT_1:def 12;
reconsider z = z as Point of [:(TOP-REAL n),I[01]:] by A53;
consider y being Point of (TOP-REAL n), j being Point of I[01] such that
A56: z = [y,j] by BORSUK_1:50;
reconsider ez = F . z, ey = y as Point of (Euclid n) by TOPREAL3:13;
reconsider fp = ep, fz = ez, fy = y as Element of REAL n by EUCLID:25;
fy in B by A54, A56, ZFMISC_1:106;
then A57: dist (lx,ey) < r0 by METRIC_1:12;
A58: ez = F . (y,j) by A56
.= j * y by A1 ;
fp = i * x by A5
.= 0. (TOP-REAL n) by A52, EUCLID:33 ;
then A59: fz - fp = (F . z) - (0. (TOP-REAL n)) by EUCLID:73
.= fz by RLVECT_1:26 ;
A60: |.fy.| - |.fx.| <= |.(fy - fx).| by EUCLID:18;
( dist (lx,ey) = |.(fx - fy).| & |.(fx - fy).| = |.(fy - fx).| ) by A6, EUCLID:21, SPPOL_1:20;
then |.fy.| - |.fx.| < r0 by A57, A60, XXREAL_0:2;
then A61: |.fy.| < |.fx.| + r0 by XREAL_1:21;

A62: now

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

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

j in X1 by A54, A56, ZFMISC_1:106;
then j < r0 / (|.fx.| + r0) by XXREAL_1:3;
then r0 / j > r0 / (r0 / (|.fx.| + r0)) by A7, A63, XREAL_1:78;
then |.fx.| + r0 < r0 / j by A45, XCMPLX_1:54;
then |.fy.| < r0 / j by A61, XXREAL_0:2;
then j * |.fy.| < j * (r0 / j) by A63, XREAL_1:70;
hence j * |.fy.| < r0 by A63, XCMPLX_1:88; :: thesis: verum

end;

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

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

end;

end;

end;

A64: 0 <= j by BORSUK_1:86;
dist (ep,ez) = |.(fz - fp).| by A6, SPPOL_1:20
.= |.fz.| by A59
.= |.(j * fy).| by A58, EUCLID:69
.= (abs j) * |.fy.| by EUCLID:14
.= j * |.fy.| by A64, ABSVALUE:def 1 ;
hence m in Ball (ep,r0) by A55, A62, METRIC_1:12; :: thesis: verum

end;

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

end;

end;

end;

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