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 = (1 - 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 = (1 - 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 = (1 - 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
.= (1 - i) * x by A1 ;

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

suppose A10: 1 - 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) / (1 - i)) as Subset of (TOP-REAL n) by TOPREAL3:13;
set t = ((2 * (1 - i)) * |.fx.|) + r0;
set c = ((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0);
set X1 = ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[;
set X2 = ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ /\ the carrier of I[01] ;
A11: 0 < 2 * (1 - i) by A10, XREAL_1:131;
then A12: 0 <= (2 * (1 - i)) * |.fx.| ;
then A13: 0 + 0 < ((2 * (1 - i)) * |.fx.|) + r0 by A6;
0 < (1 - i) * r0 by A6, A10, XREAL_1:131;
then A14: 0 < ((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0) by A13, XREAL_1:141;
reconsider X2 = ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - 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) < ((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0) by A14, ABSVALUE:def 1;
then i in ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - 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 )
0 <= i by BORSUK_1:86;
then A16: 0 <= i * ((2 * (1 - i)) * |.fx.|) by A12;
A17: (((i * 2) * (1 - i)) * |.fx.|) + 0 <= (((i * 2) * (1 - i)) * |.fx.|) + r0 by A6, XREAL_1:8;
A18: i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) = ((i * (((2 * (1 - i)) * |.fx.|) + r0)) / (((2 * (1 - i)) * |.fx.|) + r0)) + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) by A13, XCMPLX_1:90
.= ((i * (((2 * (1 - i)) * |.fx.|) + r0)) + ((1 - i) * r0)) / (((2 * (1 - i)) * |.fx.|) + r0) by XCMPLX_1:63
.= ((((i * 2) * (1 - i)) * |.fx.|) + r0) / (((2 * (1 - i)) * |.fx.|) + r0) ;
then A19: 0 <= i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) by A13, A16, A17;
A20: (i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))) - 1 = (((((i * 2) * (1 - i)) * |.fx.|) + r0) / (((2 * (1 - i)) * |.fx.|) + r0)) - ((((2 * (1 - i)) * |.fx.|) + r0) / (((2 * (1 - i)) * |.fx.|) + r0)) by A13, A18, XCMPLX_1:60
.= (((((i * 2) * (1 - i)) * |.fx.|) + r0) - (((2 * (1 - i)) * |.fx.|) + r0)) / (((2 * (1 - i)) * |.fx.|) + r0) by XCMPLX_1:121 ;
- (- (1 - i)) > - 0 by A10;
then - (1 - i) < 0 ;
then (i - 1) * ((2 * (1 - i)) * |.fx.|) <= 0 by A11;
then (i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))) - 1 <= 0 by A13, A20;
then A21: ((i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))) - 1) + 1 <= 0 + 1 by XREAL_1:9;
then A22: i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) is Point of I[01] by A19, BORSUK_1:86;

A23: now

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

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

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

proof

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

end;

then reconsider X1 = ].(i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))),(i + (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0))).[ as Subset of I[01] ;

now

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

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

then i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) <= 1 by A21, XXREAL_0:2;
then i - (((1 - i) * r0) / (((2 * (1 - i)) * |.fx.|) + r0)) is Point of I[01] by A24, BORSUK_1:86;
hence X1 is open by A22, BORSUK_4:70; :: thesis: verum

end;

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

then X1 = {} I[01] by XXREAL_1:28;
hence X1 is open ; :: thesis: verum

end;

end;

end;

hence X2 is open by A2, TOPS_1:38; :: thesis: verum

end;

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

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

proof

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

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

end;

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

end;

hence X2 is open by A22, Th5; :: thesis: verum

end;

end;

end;

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

end;

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

end;

suppose 1 - 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 A50: (1 - i) + i <= 0 + i by XREAL_1:8;
i <= 1 by BORSUK_1:86;
then A51: i = 1 by A50, XXREAL_0:1;
A52: 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 = ].(1 - (r0 / (|.fx.| + r0))),1.];
A53: 0 < r0 / (|.fx.| + r0) by A6, XREAL_1:141;
0 + r0 <= |.fx.| + r0 by XREAL_1:9;
then A54: r0 / (|.fx.| + r0) <= 1 by A6, XREAL_1:187;
then A55: (r0 / (|.fx.| + r0)) - (r0 / (|.fx.| + r0)) <= 1 - (r0 / (|.fx.| + r0)) by XREAL_1:11;
r0 / (|.fx.| + r0) is Point of I[01] by A53, A54, BORSUK_1:86;
then A56: 1 - (r0 / (|.fx.| + r0)) is Point of I[01] by JORDAN5B:4;
].(1 - (r0 / (|.fx.| + r0))),1.] c= the carrier of I[01]

proof

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

end;

then reconsider X1 = ].(1 - (r0 / (|.fx.| + r0))),1.] as Subset of I[01] ;
take W = [:B,X1:]; :: thesis: ( p in W & W is open & F .: W c= V )
A59: x in B by A6, GOBOARD6:4;
1 - (r0 / (|.fx.| + r0)) < 1 - 0 by A53, XREAL_1:17;
then i in X1 by A51, XXREAL_1:2;
hence p in W by A5, A59, ZFMISC_1:106; :: thesis: ( W is open & F .: W c= V )
A60: X1 is open by A56, Th4;
B is open by A52, GOBOARD6:6;
hence W is open by A60, 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
A61: z in dom F and
A62: z in W and
A63: F . z = m by FUNCT_1:def 12;
reconsider z = z as Point of [:(TOP-REAL n),I[01] :] by A61;
consider y being Point of (TOP-REAL n), j being Point of I[01] such that
A64: z = [y,j] by BORSUK_1:50;
reconsider ez = F . z, ey = y as Point of (Euclid n) by TOPREAL3:13;
A65: ez = F . y,j by A64
.= (1 - j) * y by A1 ;
reconsider fp = ep, fz = ez, fy = y as Element of REAL n by EUCLID:25;
A66: (F . z) - (0. (TOP-REAL n)) = F . z by RLVECT_1:26, RLVECT_1:27;
1 - j is Point of I[01] by JORDAN5B:4;
then A67: 0 <= 1 - j by BORSUK_1:86;
X1: fz = F . z ;
fp = (1 - i) * x by A9
.= 0. (TOP-REAL n) by A51, EUCLID:33 ;
then A68: fz - fp = (F . z) - (0. (TOP-REAL n)) by A66, EUCLID:73, X1
.= fz by A9, A51, A66, EUCLID:33 ;
X2: |.((1 - j) * fy).| = (abs (1 - j)) * |.fy.| by EUCLID:14;
A69: dist ep,ez = |.(fz - fp).| by SPPOL_1:20
.= |.fz.| by A68
.= |.((1 - j) * fy).| by A65, A68, EUCLID:69
.= (abs (1 - j)) * |.fy.| by A65, A68, X2
.= (1 - j) * |.fy.| by A67, ABSVALUE:def 1 ;
fy in B by A62, A64, ZFMISC_1:106;
then A70: dist lx,ey < r0 by METRIC_1:12;
A71: dist lx,ey = |.(fx - fy).| by SPPOL_1:20;
A72: |.(fx - fy).| = |.(fy - fx).| by EUCLID:21;
|.fy.| - |.fx.| <= |.(fy - fx).| by EUCLID:18;
then |.fy.| - |.fx.| < r0 by A70, A71, A72, XXREAL_0:2;
then A73: |.fy.| < |.fx.| + r0 by XREAL_1:21;

now

per cases ( j < 1 or j >= 1 ) ;

suppose j < 1 ; :: thesis: (1 - j) * |.fy.| < r0

then A74: j - j < 1 - j by XREAL_1:16;
j in X1 by A62, A64, ZFMISC_1:106;
then 1 - (r0 / (|.fx.| + r0)) < j by XXREAL_1:2;
then (1 - (r0 / (|.fx.| + r0))) + (r0 / (|.fx.| + r0)) < j + (r0 / (|.fx.| + r0)) by XREAL_1:10;
then 1 - j < (j + (r0 / (|.fx.| + r0))) - j by XREAL_1:16;
then r0 / (1 - j) > r0 / (r0 / (|.fx.| + r0)) by A6, A74, XREAL_1:78;
then |.fx.| + r0 < r0 / (1 - j) by A53, XCMPLX_1:54;
then |.fy.| < r0 / (1 - j) by A73, XXREAL_0:2;
then (1 - j) * |.fy.| < (1 - j) * (r0 / (1 - j)) by A74, XREAL_1:70;
hence (1 - j) * |.fy.| < r0 by A74, XCMPLX_1:88; :: thesis: verum

end;

suppose A75: j >= 1 ; :: thesis: (1 - j) * |.fy.| < r0

j <= 1 by BORSUK_1:86;
then j = 1 by A75, XXREAL_0:1;
hence (1 - j) * |.fy.| < r0 by A6; :: thesis: verum

end;

end;

end;

hence m in Ball ep,r0 by A63, A69, 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