:: LOPBAN_6 semantic presentation

begin

theorem Th1: :: LOPBAN_6:1
for x, y being real number st 0 <= x & x < y holds
ex s0 being real number st
( 0 < s0 & x < y / (1 + s0) & y / (1 + s0) < y )
proof
let x, y be real number ; ::_thesis: ( 0 <= x & x < y implies ex s0 being real number st
( 0 < s0 & x < y / (1 + s0) & y / (1 + s0) < y ) )
assume that
A1: 0 <= x and
A2: x < y ; ::_thesis: ex s0 being real number st
( 0 < s0 & x < y / (1 + s0) & y / (1 + s0) < y )
 ex s0 being real number st
( 0 < s0 & x < y / (1 + s0) & y / (1 + s0) < y )
proof
consider s being real number  such that
A3: x < s and
A4: s < y by A2, XREAL_1:5;
now__::_thesis:_(_(_0_=_x_&_0_<_s_&_x_<_y_/_(1_+_s)_&_y_/_(1_+_s)_<_y_)_or_(_0_<_x_&_0_<_(s_/_x)_-_1_&_x_<_y_/_(1_+_((s_/_x)_-_1))_&_y_/_(1_+_((s_/_x)_-_1))_<_y_)_)
percases ( 0 = x or 0 < x ) by A1;
caseA5: 0 = x ; ::_thesis: ( 0 < s & x < y / (1 + s) & y / (1 + s) < y )
set s0 = s;
 y < y * (1 + s) by A1, A3, A4, XREAL_1:29, XREAL_1:155;
hence  ( 0 < s & x < y / (1 + s) & y / (1 + s) < y ) by A3, A4, A5, XREAL_1:83, XREAL_1:139; ::_thesis: verum
end;
caseA6: 0 < x ; ::_thesis: ( 0 < (s / x) - 1 & x < y / (1 + ((s / x) - 1)) & y / (1 + ((s / x) - 1)) < y )
set s0 = (s / x) - 1;
A7: (1 + ((s / x) - 1)) " = 1 / (1 + ((s / x) - 1)) by XCMPLX_1:215;
then A8: s * ((1 + ((s / x) - 1)) ") = (s * 1) / (1 + ((s / x) - 1)) by XCMPLX_1:74;
 (1 + ((s / x) - 1)) * x = (x / x) * s by XCMPLX_1:75;
then  (1 + ((s / x) - 1)) * x = 1 * s by A6, XCMPLX_1:60;
then A9: (((1 + ((s / x) - 1)) ") * (1 + ((s / x) - 1))) * x = s * ((1 + ((s / x) - 1)) ") ;
 0 < 1 + ((s / x) - 1) by A3, A6, XREAL_1:187;
then A10: ((1 + ((s / x) - 1)) ") * (1 + ((s / x) - 1)) = 1 by A7, XCMPLX_1:106;
A11: 1 < 1 + ((s / x) - 1) by A3, A6, XREAL_1:187;
then  y < y * (1 + ((s / x) - 1)) by A1, A2, XREAL_1:155;
hence  ( 0 < (s / x) - 1 & x < y / (1 + ((s / x) - 1)) & y / (1 + ((s / x) - 1)) < y ) by A4, A11, A9, A10, A8, XREAL_1:50, XREAL_1:74, XREAL_1:83; ::_thesis: verum
end;
end;
end;
hence  ex s0 being real number st
( 0 < s0 & x < y / (1 + s0) & y / (1 + s0) < y ) ; ::_thesis: verum
end;
hence  ex s0 being real number st
( 0 < s0 & x < y / (1 + s0) & y / (1 + s0) < y ) ; ::_thesis: verum
end;

scheme :: LOPBAN_6:sch 1
RecExD3{ F1() ->  non empty set , F2() ->  Element of F1(), F3() ->  Element of F1(), P1[ set , set , set , set ] } :
 ex f being Function of NAT,F1() st
( f . 0 = F2() & f . 1 = F3() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1),f . (n + 2)] ) )
provided
A1: for n being Element of NAT
for x, y being Element of F1() ex z being Element of F1() st P1[n,x,y,z]
proof
defpred S1[ set , set , set ] means ( P1[$1,$2 `1 ,$2 `2 ,$3 `2 ] & $2 `2 = $3 `1 );
A2: for n being Element of NAT
for x being Element of [:F1(),F1():] ex y being Element of [:F1(),F1():] st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being Element of [:F1(),F1():] ex y being Element of [:F1(),F1():] st S1[n,x,y]
let x be Element of [:F1(),F1():]; ::_thesis: ex y being Element of [:F1(),F1():] st S1[n,x,y]
set z = x `1 ;
set w = x `2 ;
reconsider z = x `1 , w = x `2 as Element of F1() ;
consider s being Element of F1() such that
A3: P1[n,z,w,s] by A1;
set y = [w,s];
reconsider y = [w,s] as Element of [:F1(),F1():] ;
take  y ; ::_thesis: S1[n,x,y]
thus  S1[n,x,y] by A3, MCART_1:7; ::_thesis: verum
end;
consider g being Function of NAT,[:F1(),F1():] such that
A4: ( g . 0 = [F2(),F3()] & ( for n being Element of NAT holds S1[n,g . n,g . (n + 1)] ) ) from RECDEF_1:sch_2(A2);
deffunc H1( Element of NAT ) ->  Element of F1() = (g . $1) `1 ;
A5: for x being Element of NAT holds H1(x) in F1() ;
consider f being Function of NAT,F1() such that
A6: for x being Element of NAT holds f . x = H1(x) from FUNCT_2:sch_8(A5);
A7: now__::_thesis:_for_n_being_Element_of_NAT_holds_P1[n,f_._n,f_._(n_+_1),f_._(n_+_2)]
let n be Element of NAT ; ::_thesis: P1[n,f . n,f . (n + 1),f . (n + 2)]
A8: f . n = (g . n) `1 by A6;
 S1[n + 1,g . (n + 1),g . ((n + 1) + 1)] by A4;
then A9: f . (n + 2) = (g . (n + 1)) `2 by A6;
f . (n + 1) = (g . (n + 1)) `1 by A6
.= (g . n) `2 by A4 ;
hence  P1[n,f . n,f . (n + 1),f . (n + 2)] by A4, A8, A9; ::_thesis: verum
end;
take  f ; ::_thesis: ( f . 0 = F2() & f . 1 = F3() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1),f . (n + 2)] ) )
A10: S1[ 0 ,g . 0,g . (0 + 1)] by A4;
A11: f . 0 = (g . 0) `1 by A6
.= F2() by A4, MCART_1:7 ;
f . 1 = (g . 1) `1 by A6
.= F3() by A4, A10, MCART_1:7 ;
hence  ( f . 0 = F2() & f . 1 = F3() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1),f . (n + 2)] ) ) by A11, A7; ::_thesis: verum
end;


theorem Th2: :: LOPBAN_6:2
for X being RealNormSpace
for y1 being Point of X
for r being real number holds Ball (y1,r) = y1 + (Ball ((0. X),r))
proof
let X be RealNormSpace; ::_thesis: for y1 being Point of X
for r being real number holds Ball (y1,r) = y1 + (Ball ((0. X),r))
let y1 be Point of X; ::_thesis: for r being real number holds Ball (y1,r) = y1 + (Ball ((0. X),r))
let r be real number ; ::_thesis: Ball (y1,r) = y1 + (Ball ((0. X),r))
thus  Ball (y1,r) c= y1 + (Ball ((0. X),r)) :: according to XBOOLE_0:def_10 ::_thesis: y1 + (Ball ((0. X),r)) c= Ball (y1,r)
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in Ball (y1,r) or t in y1 + (Ball ((0. X),r)) )
assume A1: t in Ball (y1,r) ; ::_thesis: t in y1 + (Ball ((0. X),r))
then reconsider z1 = t as Point of X ;
set z0 = z1 - y1;
 ex zz1 being Point of X st
( z1 = zz1 & ||.(y1 - zz1).|| < r ) by A1;
then  ||.(- (z1 - y1)).|| < r by RLVECT_1:33;
then  ||.((0. X) - (z1 - y1)).|| < r by RLVECT_1:14;
then A2: z1 - y1 in Ball ((0. X),r) ;
 (z1 - y1) + y1 = z1 + ((- y1) + y1) by RLVECT_1:def_3;
then  (z1 - y1) + y1 = z1 + (0. X) by RLVECT_1:5;
then  z1 = (z1 - y1) + y1 by RLVECT_1:4;
hence  t in y1 + (Ball ((0. X),r)) by A2; ::_thesis: verum
end;
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in y1 + (Ball ((0. X),r)) or t in Ball (y1,r) )
assume  t in y1 + (Ball ((0. X),r)) ; ::_thesis: t in Ball (y1,r)
then consider z0 being Point of X such that
A3: t = y1 + z0 and
A4: z0 in Ball ((0. X),r) ;
set z1 = z0 + y1;
 ex zz0 being Point of X st
( z0 = zz0 & ||.((0. X) - zz0).|| < r ) by A4;
then  ||.(- z0).|| < r by RLVECT_1:14;
then  ||.z0.|| < r by NORMSP_1:2;
then  ||.(z0 + (0. X)).|| < r by RLVECT_1:4;
then  ||.(z0 + (y1 + (- y1))).|| < r by RLVECT_1:5;
then  ||.((z0 + y1) - y1).|| < r by RLVECT_1:def_3;
then  ||.(y1 - (z0 + y1)).|| < r by NORMSP_1:7;
hence  t in Ball (y1,r) by A3; ::_thesis: verum
end;

theorem Th3: :: LOPBAN_6:3
for X being RealNormSpace
for r being real number
for a being Real st 0 < a holds
Ball ((0. X),(a * r)) = a * (Ball ((0. X),r))
proof
let X be RealNormSpace; ::_thesis: for r being real number
for a being Real st 0 < a holds
Ball ((0. X),(a * r)) = a * (Ball ((0. X),r))
let r be real number ; ::_thesis: for a being Real st 0 < a holds
Ball ((0. X),(a * r)) = a * (Ball ((0. X),r))
let a be Real; ::_thesis: ( 0 < a implies Ball ((0. X),(a * r)) = a * (Ball ((0. X),r)) )
assume A1: 0 < a ; ::_thesis: Ball ((0. X),(a * r)) = a * (Ball ((0. X),r))
thus  Ball ((0. X),(a * r)) c= a * (Ball ((0. X),r)) :: according to XBOOLE_0:def_10 ::_thesis: a * (Ball ((0. X),r)) c= Ball ((0. X),(a * r))
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Ball ((0. X),(a * r)) or z in a * (Ball ((0. X),r)) )
assume A2: z in Ball ((0. X),(a * r)) ; ::_thesis: z in a * (Ball ((0. X),r))
then reconsider z1 = z as Point of X ;
 ex zz1 being Point of X st
( z1 = zz1 & ||.((0. X) - zz1).|| < a * r ) by A2;
then  ||.(- z1).|| < a * r by RLVECT_1:14;
then  ||.z1.|| < a * r by NORMSP_1:2;
then  (a ") * ||.z1.|| < (a ") * (a * r) by A1, XREAL_1:68;
then  (a ") * ||.z1.|| < (a * (a ")) * r ;
then A3: (a ") * ||.z1.|| < 1 * r by A1, XCMPLX_0:def_7;
set y1 = (a ") * z1;
||.((a ") * z1).|| = (abs (a ")) * ||.z1.|| by NORMSP_1:def_1
.= (a ") * ||.z1.|| by A1, ABSVALUE:def_1 ;
then  ||.(- ((a ") * z1)).|| < r by A3, NORMSP_1:2;
then  ||.((0. X) - ((a ") * z1)).|| < r by RLVECT_1:14;
then A4: (a ") * z1 in Ball ((0. X),r) ;
a * ((a ") * z1) = (a * (a ")) * z1 by RLVECT_1:def_7
.= 1 * z1 by A1, XCMPLX_0:def_7
.= z1 by RLVECT_1:def_8 ;
hence  z in a * (Ball ((0. X),r)) by A4; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in a * (Ball ((0. X),r)) or z in Ball ((0. X),(a * r)) )
assume A5: z in a * (Ball ((0. X),r)) ; ::_thesis: z in Ball ((0. X),(a * r))
then reconsider z1 = z as Point of X ;
consider y1 being Point of X such that
A6: z1 = a * y1 and
A7: y1 in Ball ((0. X),r) by A5;
 ex yy1 being Point of X st
( y1 = yy1 & ||.((0. X) - yy1).|| < r ) by A7;
then  ||.(- y1).|| < r by RLVECT_1:14;
then A8: ||.y1.|| < r by NORMSP_1:2;
||.z1.|| = (abs a) * ||.y1.|| by A6, NORMSP_1:def_1
.= a * ||.y1.|| by A1, ABSVALUE:def_1 ;
then  ||.z1.|| < a * r by A1, A8, XREAL_1:68;
then  ||.(- z1).|| < a * r by NORMSP_1:2;
then  ||.((0. X) - z1).|| < a * r by RLVECT_1:14;
hence  z in Ball ((0. X),(a * r)) ; ::_thesis: verum
end;

theorem :: LOPBAN_6:4
for X, Y being RealNormSpace
for T being LinearOperator of X,Y
for B0, B1 being Subset of X holds T .: (B0 + B1) = (T .: B0) + (T .: B1)
proof
let X, Y be RealNormSpace; ::_thesis: for T being LinearOperator of X,Y
for B0, B1 being Subset of X holds T .: (B0 + B1) = (T .: B0) + (T .: B1)
let T be LinearOperator of X,Y; ::_thesis: for B0, B1 being Subset of X holds T .: (B0 + B1) = (T .: B0) + (T .: B1)
let B0, B1 be Subset of X; ::_thesis: T .: (B0 + B1) = (T .: B0) + (T .: B1)
thus  T .: (B0 + B1) c= (T .: B0) + (T .: B1) :: according to XBOOLE_0:def_10 ::_thesis: (T .: B0) + (T .: B1) c= T .: (B0 + B1)
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in T .: (B0 + B1) or t in (T .: B0) + (T .: B1) )
assume  t in T .: (B0 + B1) ; ::_thesis: t in (T .: B0) + (T .: B1)
then consider z1 being set  such that
 z1 in the carrier of X and
A1: z1 in B0 + B1 and
A2: t = T . z1 by FUNCT_2:64;
consider x1, x2 being Element of X such that
A3: z1 = x1 + x2 and
A4: ( x1 in B0 & x2 in B1 ) by A1;
A5: ( T . x1 in T .: B0 & T . x2 in T .: B1 ) by A4, FUNCT_2:35;
 t = (T . x1) + (T . x2) by A2, A3, VECTSP_1:def_20;
hence  t in (T .: B0) + (T .: B1) by A5; ::_thesis: verum
end;
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in (T .: B0) + (T .: B1) or t in T .: (B0 + B1) )
assume  t in (T .: B0) + (T .: B1) ; ::_thesis: t in T .: (B0 + B1)
then consider tz0, tz1 being Point of Y such that
A6: t = tz0 + tz1 and
A7: tz0 in T .: B0 and
A8: tz1 in T .: B1 ;
consider z1 being Element of X such that
A9: z1 in B1 and
A10: tz1 = T . z1 by A8, FUNCT_2:65;
consider z0 being Element of X such that
A11: z0 in B0 and
A12: tz0 = T . z0 by A7, FUNCT_2:65;
reconsider z1 = z1 as Point of X ;
reconsider z0 = z0 as Point of X ;
A13: z0 + z1 in B0 + B1 by A11, A9;
 t = T . (z0 + z1) by A6, A12, A10, VECTSP_1:def_20;
hence  t in T .: (B0 + B1) by A13, FUNCT_2:35; ::_thesis: verum
end;

theorem Th5: :: LOPBAN_6:5
for X, Y being RealNormSpace
for T being LinearOperator of X,Y
for B0 being Subset of X
for a being Real holds T .: (a * B0) = a * (T .: B0)
proof
let X, Y be RealNormSpace; ::_thesis: for T being LinearOperator of X,Y
for B0 being Subset of X
for a being Real holds T .: (a * B0) = a * (T .: B0)
let T be LinearOperator of X,Y; ::_thesis: for B0 being Subset of X
for a being Real holds T .: (a * B0) = a * (T .: B0)
let B0 be Subset of X; ::_thesis: for a being Real holds T .: (a * B0) = a * (T .: B0)
let a be Real; ::_thesis: T .: (a * B0) = a * (T .: B0)
thus  T .: (a * B0) c= a * (T .: B0) :: according to XBOOLE_0:def_10 ::_thesis: a * (T .: B0) c= T .: (a * B0)
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in T .: (a * B0) or t in a * (T .: B0) )
assume  t in T .: (a * B0) ; ::_thesis: t in a * (T .: B0)
then consider z1 being set  such that
 z1 in the carrier of X and
A1: z1 in a * B0 and
A2: t = T . z1 by FUNCT_2:64;
consider x1 being Element of X such that
A3: z1 = a * x1 and
A4: x1 in B0 by A1;
A5: T . x1 in T .: B0 by A4, FUNCT_2:35;
 t = a * (T . x1) by A2, A3, LOPBAN_1:def_5;
hence  t in a * (T .: B0) by A5; ::_thesis: verum
end;
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in a * (T .: B0) or t in T .: (a * B0) )
assume  t in a * (T .: B0) ; ::_thesis: t in T .: (a * B0)
then consider tz0 being Point of Y such that
A6: t = a * tz0 and
A7: tz0 in T .: B0 ;
consider z0 being Element of X such that
A8: z0 in B0 and
A9: tz0 = T . z0 by A7, FUNCT_2:65;
reconsider z0 = z0 as Point of X ;
set z1 = a * z0;
A10: a * z0 in a * B0 by A8;
 t = T . (a * z0) by A6, A9, LOPBAN_1:def_5;
hence  t in T .: (a * B0) by A10, FUNCT_2:35; ::_thesis: verum
end;

theorem Th6: :: LOPBAN_6:6
for X, Y being RealNormSpace
for T being LinearOperator of X,Y
for B0 being Subset of X
for x1 being Point of X holds T .: (x1 + B0) = (T . x1) + (T .: B0)
proof
let X, Y be RealNormSpace; ::_thesis: for T being LinearOperator of X,Y
for B0 being Subset of X
for x1 being Point of X holds T .: (x1 + B0) = (T . x1) + (T .: B0)
let T be LinearOperator of X,Y; ::_thesis: for B0 being Subset of X
for x1 being Point of X holds T .: (x1 + B0) = (T . x1) + (T .: B0)
let B0 be Subset of X; ::_thesis: for x1 being Point of X holds T .: (x1 + B0) = (T . x1) + (T .: B0)
let x1 be Point of X; ::_thesis: T .: (x1 + B0) = (T . x1) + (T .: B0)
thus  T .: (x1 + B0) c= (T . x1) + (T .: B0) :: according to XBOOLE_0:def_10 ::_thesis: (T . x1) + (T .: B0) c= T .: (x1 + B0)
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in T .: (x1 + B0) or t in (T . x1) + (T .: B0) )
assume  t in T .: (x1 + B0) ; ::_thesis: t in (T . x1) + (T .: B0)
then consider z1 being set  such that
A1: z1 in the carrier of X and
A2: z1 in x1 + B0 and
A3: t = T . z1 by FUNCT_2:64;
reconsider z1 = z1 as Point of X by A1;
consider z0 being Element of X such that
A4: z1 = x1 + z0 and
A5: z0 in B0 by A2;
A6: T . z0 in T .: B0 by A5, FUNCT_2:35;
 t = (T . x1) + (T . z0) by A3, A4, VECTSP_1:def_20;
hence  t in (T . x1) + (T .: B0) by A6; ::_thesis: verum
end;
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in (T . x1) + (T .: B0) or t in T .: (x1 + B0) )
assume  t in (T . x1) + (T .: B0) ; ::_thesis: t in T .: (x1 + B0)
then consider tz0 being Point of Y such that
A7: t = (T . x1) + tz0 and
A8: tz0 in T .: B0 ;
consider z0 being Element of X such that
A9: z0 in B0 and
A10: tz0 = T . z0 by A8, FUNCT_2:65;
A11: x1 + z0 in x1 + B0 by A9;
 t = T . (x1 + z0) by A7, A10, VECTSP_1:def_20;
hence  t in T .: (x1 + B0) by A11, FUNCT_2:35; ::_thesis: verum
end;

theorem :: LOPBAN_6:7
for X being RealNormSpace
for V, W being Subset of X
for V1, W1 being Subset of (LinearTopSpaceNorm X) st V = V1 & W = W1 holds
V + W = V1 + W1
proof
let X be RealNormSpace; ::_thesis: for V, W being Subset of X
for V1, W1 being Subset of (LinearTopSpaceNorm X) st V = V1 & W = W1 holds
V + W = V1 + W1
let V, W be Subset of X; ::_thesis: for V1, W1 being Subset of (LinearTopSpaceNorm X) st V = V1 & W = W1 holds
V + W = V1 + W1
let V1, W1 be Subset of (LinearTopSpaceNorm X); ::_thesis: ( V = V1 & W = W1 implies V + W = V1 + W1 )
assume that
A1: V = V1 and
A2: W = W1 ; ::_thesis: V + W = V1 + W1
thus  V + W c= V1 + W1 :: according to XBOOLE_0:def_10 ::_thesis: V1 + W1 c= V + W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in V + W or x in V1 + W1 )
assume  x in V + W ; ::_thesis: x in V1 + W1
then consider u, v being Point of X such that
A3: x = u + v and
A4: u in V and
A5: v in W ;
reconsider v1 = v as Point of (LinearTopSpaceNorm X) by A2, A5;
reconsider u1 = u as Point of (LinearTopSpaceNorm X) by A1, A4;
 u + v = u1 + v1 by NORMSP_2:def_4;
hence  x in V1 + W1 by A1, A2, A3, A4, A5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in V1 + W1 or x in V + W )
assume  x in V1 + W1 ; ::_thesis: x in V + W
then consider u, v being Point of (LinearTopSpaceNorm X) such that
A6: x = u + v and
A7: u in V1 and
A8: v in W1 ;
reconsider v1 = v as Point of X by A2, A8;
reconsider u1 = u as Point of X by A1, A7;
 u + v = u1 + v1 by NORMSP_2:def_4;
hence  x in V + W by A1, A2, A6, A7, A8; ::_thesis: verum
end;

theorem Th8: :: LOPBAN_6:8
for X being RealNormSpace
for V being Subset of X
for x being Point of X
for V1 being Subset of (LinearTopSpaceNorm X)
for x1 being Point of (LinearTopSpaceNorm X) st V = V1 & x = x1 holds
x + V = x1 + V1
proof
let X be RealNormSpace; ::_thesis: for V being Subset of X
for x being Point of X
for V1 being Subset of (LinearTopSpaceNorm X)
for x1 being Point of (LinearTopSpaceNorm X) st V = V1 & x = x1 holds
x + V = x1 + V1
let V be Subset of X; ::_thesis: for x being Point of X
for V1 being Subset of (LinearTopSpaceNorm X)
for x1 being Point of (LinearTopSpaceNorm X) st V = V1 & x = x1 holds
x + V = x1 + V1
let x be Point of X; ::_thesis: for V1 being Subset of (LinearTopSpaceNorm X)
for x1 being Point of (LinearTopSpaceNorm X) st V = V1 & x = x1 holds
x + V = x1 + V1
let V1 be Subset of (LinearTopSpaceNorm X); ::_thesis: for x1 being Point of (LinearTopSpaceNorm X) st V = V1 & x = x1 holds
x + V = x1 + V1
let x1 be Point of (LinearTopSpaceNorm X); ::_thesis: ( V = V1 & x = x1 implies x + V = x1 + V1 )
assume that
A1: V = V1 and
A2: x = x1 ; ::_thesis: x + V = x1 + V1
thus  x + V c= x1 + V1 :: according to XBOOLE_0:def_10 ::_thesis: x1 + V1 c= x + V
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in x + V or z in x1 + V1 )
assume  z in x + V ; ::_thesis: z in x1 + V1
then consider u being Point of X such that
A3: z = x + u and
A4: u in V ;
reconsider u1 = u as Point of (LinearTopSpaceNorm X) by A1, A4;
 x + u = x1 + u1 by A2, NORMSP_2:def_4;
hence  z in x1 + V1 by A1, A3, A4; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in x1 + V1 or z in x + V )
assume  z in x1 + V1 ; ::_thesis: z in x + V
then consider u1 being Point of (LinearTopSpaceNorm X) such that
A5: z = x1 + u1 and
A6: u1 in V1 ;
reconsider u = u1 as Point of X by A1, A6;
 x1 + u1 = x + u by A2, NORMSP_2:def_4;
hence  z in x + V by A1, A5, A6; ::_thesis: verum
end;

theorem Th9: :: LOPBAN_6:9
for X being RealNormSpace
for V being Subset of X
for a being Real
for V1 being Subset of (LinearTopSpaceNorm X) st V = V1 holds
a * V = a * V1
proof
let X be RealNormSpace; ::_thesis: for V being Subset of X
for a being Real
for V1 being Subset of (LinearTopSpaceNorm X) st V = V1 holds
a * V = a * V1
let V be Subset of X; ::_thesis: for a being Real
for V1 being Subset of (LinearTopSpaceNorm X) st V = V1 holds
a * V = a * V1
let a be Real; ::_thesis: for V1 being Subset of (LinearTopSpaceNorm X) st V = V1 holds
a * V = a * V1
let V1 be Subset of (LinearTopSpaceNorm X); ::_thesis: ( V = V1 implies a * V = a * V1 )
assume A1: V = V1 ; ::_thesis: a * V = a * V1
thus  a * V c= a * V1 :: according to XBOOLE_0:def_10 ::_thesis: a * V1 c= a * V
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in a * V or z in a * V1 )
assume  z in a * V ; ::_thesis: z in a * V1
then consider v being Point of X such that
A2: z = a * v and
A3: v in V ;
reconsider v1 = v as Point of (LinearTopSpaceNorm X) by A1, A3;
 a * v = a * v1 by NORMSP_2:def_4;
hence  z in a * V1 by A1, A2, A3; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in a * V1 or z in a * V )
assume  z in a * V1 ; ::_thesis: z in a * V
then consider v being Point of (LinearTopSpaceNorm X) such that
A4: z = a * v and
A5: v in V1 ;
reconsider v1 = v as Point of X by A1, A5;
 a * v = a * v1 by NORMSP_2:def_4;
hence  z in a * V by A1, A4, A5; ::_thesis: verum
end;

theorem Th10: :: LOPBAN_6:10
for X being RealNormSpace
for V being Subset of (TopSpaceNorm X)
for V1 being Subset of (LinearTopSpaceNorm X) st V = V1 holds
Cl V = Cl V1
proof
let X be RealNormSpace; ::_thesis: for V being Subset of (TopSpaceNorm X)
for V1 being Subset of (LinearTopSpaceNorm X) st V = V1 holds
Cl V = Cl V1
let V be Subset of (TopSpaceNorm X); ::_thesis: for V1 being Subset of (LinearTopSpaceNorm X) st V = V1 holds
Cl V = Cl V1
let V1 be Subset of (LinearTopSpaceNorm X); ::_thesis: ( V = V1 implies Cl V = Cl V1 )
assume A1: V = V1 ; ::_thesis: Cl V = Cl V1
thus  Cl V c= Cl V1 :: according to XBOOLE_0:def_10 ::_thesis: Cl V1 c= Cl V
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Cl V or z in Cl V1 )
assume A2: z in Cl V ; ::_thesis: z in Cl V1
A3: for D1 being Subset of (LinearTopSpaceNorm X) st D1 is closed & V1 c= D1 holds
z in D1
proof
let D1 be Subset of (LinearTopSpaceNorm X); ::_thesis: ( D1 is closed & V1 c= D1 implies z in D1 )
assume A4: D1 is closed ; ::_thesis: ( not V1 c= D1 or z in D1 )
reconsider D0 = D1 as Subset of X by NORMSP_2:def_4;
reconsider D2 = D1 as Subset of (TopSpaceNorm X) by NORMSP_2:def_4;
 D0 is closed by A4, NORMSP_2:32;
then A5: D2 is closed by NORMSP_2:15;
assume  V1 c= D1 ; ::_thesis: z in D1
hence  z in D1 by A1, A2, A5, PRE_TOPC:15; ::_thesis: verum
end;
 z in the carrier of X by A2;
then  z in the carrier of (LinearTopSpaceNorm X) by NORMSP_2:def_4;
hence  z in Cl V1 by A3, PRE_TOPC:15; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Cl V1 or z in Cl V )
assume A6: z in Cl V1 ; ::_thesis: z in Cl V
A7: for D1 being Subset of (TopSpaceNorm X) st D1 is closed & V c= D1 holds
z in D1
proof
let D1 be Subset of (TopSpaceNorm X); ::_thesis: ( D1 is closed & V c= D1 implies z in D1 )
assume A8: D1 is closed ; ::_thesis: ( not V c= D1 or z in D1 )
reconsider D0 = D1 as Subset of X ;
reconsider D2 = D1 as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def_4;
 D0 is closed by A8, NORMSP_2:15;
then A9: D2 is closed by NORMSP_2:32;
assume  V c= D1 ; ::_thesis: z in D1
hence  z in D1 by A1, A6, A9, PRE_TOPC:15; ::_thesis: verum
end;
 z in the carrier of (LinearTopSpaceNorm X) by A6;
then  z in the carrier of (TopSpaceNorm X) by NORMSP_2:def_4;
hence  z in Cl V by A7, PRE_TOPC:15; ::_thesis: verum
end;

theorem Th11: :: LOPBAN_6:11
for X being RealNormSpace
for x being Point of X
for r being real number holds Ball ((0. X),r) = (- 1) * (Ball ((0. X),r))
proof
let X be RealNormSpace; ::_thesis: for x being Point of X
for r being real number holds Ball ((0. X),r) = (- 1) * (Ball ((0. X),r))
let x be Point of X; ::_thesis: for r being real number holds Ball ((0. X),r) = (- 1) * (Ball ((0. X),r))
let r be real number ; ::_thesis: Ball ((0. X),r) = (- 1) * (Ball ((0. X),r))
thus  Ball ((0. X),r) c= (- 1) * (Ball ((0. X),r)) :: according to XBOOLE_0:def_10 ::_thesis: (- 1) * (Ball ((0. X),r)) c= Ball ((0. X),r)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Ball ((0. X),r) or z in (- 1) * (Ball ((0. X),r)) )
assume A1: z in Ball ((0. X),r) ; ::_thesis: z in (- 1) * (Ball ((0. X),r))
then reconsider z1 = z as Point of X ;
 ex zz1 being Point of X st
( z1 = zz1 & ||.((0. X) - zz1).|| < r ) by A1;
then  ||.(- z1).|| < r by RLVECT_1:14;
then  ||.(- (- z1)).|| < r by NORMSP_1:2;
then  ||.((0. X) - (- z1)).|| < r by RLVECT_1:14;
then A2: - z1 in Ball ((0. X),r) ;
(- 1) * (- z1) = 1 * z1 by RLVECT_1:26
.= z1 by RLVECT_1:def_8 ;
hence  z in (- 1) * (Ball ((0. X),r)) by A2; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in (- 1) * (Ball ((0. X),r)) or z in Ball ((0. X),r) )
assume A3: z in (- 1) * (Ball ((0. X),r)) ; ::_thesis: z in Ball ((0. X),r)
then reconsider z1 = z as Point of X ;
consider y1 being Point of X such that
A4: z1 = (- 1) * y1 and
A5: y1 in Ball ((0. X),r) by A3;
 ex zz1 being Point of X st
( y1 = zz1 & ||.((0. X) - zz1).|| < r ) by A5;
then  ||.(- y1).|| < r by RLVECT_1:14;
then  ||.(- (- y1)).|| < r by NORMSP_1:2;
then A6: ||.((0. X) - (- y1)).|| < r by RLVECT_1:14;
 - y1 = z1 by A4, RLVECT_1:16;
hence  z in Ball ((0. X),r) by A6; ::_thesis: verum
end;

theorem Th12: :: LOPBAN_6:12
for X being RealNormSpace
for x being Point of X
for r being real number
for V being Subset of (LinearTopSpaceNorm X) st V = Ball (x,r) holds
V is convex
proof
let X be RealNormSpace; ::_thesis: for x being Point of X
for r being real number
for V being Subset of (LinearTopSpaceNorm X) st V = Ball (x,r) holds
V is convex
let x be Point of X; ::_thesis: for r being real number
for V being Subset of (LinearTopSpaceNorm X) st V = Ball (x,r) holds
V is convex
let r be real number ; ::_thesis: for V being Subset of (LinearTopSpaceNorm X) st V = Ball (x,r) holds
V is convex
let V be Subset of (LinearTopSpaceNorm X); ::_thesis: ( V = Ball (x,r) implies V is convex )
reconsider V1 = Ball (x,r) as Subset of X ;
A1: for u, v being Point of X
for s being Real st 0 < s & s < 1 & u in V1 & v in V1 holds
(s * u) + ((1 - s) * v) in V1
proof
let u, v be Point of X; ::_thesis: for s being Real st 0 < s & s < 1 & u in V1 & v in V1 holds
(s * u) + ((1 - s) * v) in V1
let s be Real; ::_thesis: ( 0 < s & s < 1 & u in V1 & v in V1 implies (s * u) + ((1 - s) * v) in V1 )
assume that
A2: 0 < s and
A3: s < 1 and
A4: u in V1 and
A5: v in V1 ; ::_thesis: (s * u) + ((1 - s) * v) in V1
A6: ex v1 being Point of X st
( v = v1 & ||.(x - v1).|| < r ) by A5;
 ( 0 < abs s & ex u1 being Point of X st
( u = u1 & ||.(x - u1).|| < r ) ) by A2, A4, ABSVALUE:def_1;
then A7: (abs s) * ||.(x - u).|| < (abs s) * r by XREAL_1:68;
 s + 0 < 1 by A3;
then A8: 1 - s > 0 by XREAL_1:20;
then  0 < abs (1 - s) by ABSVALUE:def_1;
then  (abs (1 - s)) * ||.(x - v).|| < (abs (1 - s)) * r by A6, XREAL_1:68;
then  ((abs s) * ||.(x - u).||) + ((abs (1 - s)) * ||.(x - v).||) < ((abs s) * r) + ((abs (1 - s)) * r) by A7, XREAL_1:8;
then  ((abs s) * ||.(x - u).||) + ((abs (1 - s)) * ||.(x - v).||) < (s * r) + ((abs (1 - s)) * r) by A2, ABSVALUE:def_1;
then  ((abs s) * ||.(x - u).||) + ((abs (1 - s)) * ||.(x - v).||) < (s * r) + ((1 - s) * r) by A8, ABSVALUE:def_1;
then  ||.(s * (x - u)).|| + ((abs (1 - s)) * ||.(x - v).||) < 1 * r by NORMSP_1:def_1;
then A9: ||.(s * (x - u)).|| + ||.((1 - s) * (x - v)).|| < r by NORMSP_1:def_1;
||.(((s * x) + ((1 - s) * x)) - ((s * u) + ((1 - s) * v))).|| = ||.(((s * x) + (- ((s * u) + ((1 - s) * v)))) + ((1 - s) * x)).|| by RLVECT_1:def_3
.= ||.(((s * x) + ((- 1) * ((s * u) + ((1 - s) * v)))) + ((1 - s) * x)).|| by RLVECT_1:16
.= ||.(((s * x) + (((- 1) * (s * u)) + ((- 1) * ((1 - s) * v)))) + ((1 - s) * x)).|| by RLVECT_1:def_5
.= ||.(((s * x) + ((- (s * u)) + ((- 1) * ((1 - s) * v)))) + ((1 - s) * x)).|| by RLVECT_1:16
.= ||.(((s * x) + ((- (s * u)) + (- ((1 - s) * v)))) + ((1 - s) * x)).|| by RLVECT_1:16
.= ||.((((s * x) + (- (s * u))) + (- ((1 - s) * v))) + ((1 - s) * x)).|| by RLVECT_1:def_3
.= ||.(((s * x) - (s * u)) + (((1 - s) * x) - ((1 - s) * v))).|| by RLVECT_1:def_3
.= ||.((s * (x - u)) + (((1 - s) * x) - ((1 - s) * v))).|| by RLVECT_1:34
.= ||.((s * (x - u)) + ((1 - s) * (x - v))).|| by RLVECT_1:34 ;
then  ||.(((s * x) + ((1 - s) * x)) - ((s * u) + ((1 - s) * v))).|| <= ||.(s * (x - u)).|| + ||.((1 - s) * (x - v)).|| by NORMSP_1:def_1;
then  ||.(((s * x) + ((1 - s) * x)) - ((s * u) + ((1 - s) * v))).|| < r by A9, XXREAL_0:2;
then  ||.(((s + (1 - s)) * x) - ((s * u) + ((1 - s) * v))).|| < r by RLVECT_1:def_6;
then  ||.(x - ((s * u) + ((1 - s) * v))).|| < r by RLVECT_1:def_8;
hence  (s * u) + ((1 - s) * v) in V1 ; ::_thesis: verum
end;
assume A10: V = Ball (x,r) ; ::_thesis: V is convex
 for u, v being Point of (LinearTopSpaceNorm X)
for s being Real st 0 < s & s < 1 & u in V & v in V holds
(s * u) + ((1 - s) * v) in V
proof
let u, v be Point of (LinearTopSpaceNorm X); ::_thesis: for s being Real st 0 < s & s < 1 & u in V & v in V holds
(s * u) + ((1 - s) * v) in V
let s be Real; ::_thesis: ( 0 < s & s < 1 & u in V & v in V implies (s * u) + ((1 - s) * v) in V )
reconsider u1 = u as Point of X by NORMSP_2:def_4;
reconsider v1 = v as Point of X by NORMSP_2:def_4;
 ( s * u1 = s * u & (1 - s) * v1 = (1 - s) * v ) by NORMSP_2:def_4;
then A11: (s * u1) + ((1 - s) * v1) = (s * u) + ((1 - s) * v) by NORMSP_2:def_4;
assume  ( 0 < s & s < 1 & u in V & v in V ) ; ::_thesis: (s * u) + ((1 - s) * v) in V
hence  (s * u) + ((1 - s) * v) in V by A10, A1, A11; ::_thesis: verum
end;
hence  V is convex by CONVEX1:def_2; ::_thesis: verum
end;

theorem Th13: :: LOPBAN_6:13
for X, Y being RealNormSpace
for x being Point of X
for r being real number
for T being LinearOperator of X,Y
for V being Subset of (LinearTopSpaceNorm Y) st V = T .: (Ball (x,r)) holds
V is convex
proof
let X, Y be RealNormSpace; ::_thesis: for x being Point of X
for r being real number
for T being LinearOperator of X,Y
for V being Subset of (LinearTopSpaceNorm Y) st V = T .: (Ball (x,r)) holds
V is convex
let x be Point of X; ::_thesis: for r being real number
for T being LinearOperator of X,Y
for V being Subset of (LinearTopSpaceNorm Y) st V = T .: (Ball (x,r)) holds
V is convex
let r be real number ; ::_thesis: for T being LinearOperator of X,Y
for V being Subset of (LinearTopSpaceNorm Y) st V = T .: (Ball (x,r)) holds
V is convex
let T be LinearOperator of X,Y; ::_thesis: for V being Subset of (LinearTopSpaceNorm Y) st V = T .: (Ball (x,r)) holds
V is convex
let V be Subset of (LinearTopSpaceNorm Y); ::_thesis: ( V = T .: (Ball (x,r)) implies V is convex )
reconsider V1 = T .: (Ball (x,r)) as Subset of Y ;
A1: for u, v being Point of Y
for s being Real st 0 < s & s < 1 & u in V1 & v in V1 holds
(s * u) + ((1 - s) * v) in V1
proof
reconsider Bxr = Ball (x,r) as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def_4;
let u, v be Point of Y; ::_thesis: for s being Real st 0 < s & s < 1 & u in V1 & v in V1 holds
(s * u) + ((1 - s) * v) in V1
let s be Real; ::_thesis: ( 0 < s & s < 1 & u in V1 & v in V1 implies (s * u) + ((1 - s) * v) in V1 )
assume that
A2: ( 0 < s & s < 1 ) and
A3: u in V1 and
A4: v in V1 ; ::_thesis: (s * u) + ((1 - s) * v) in V1
consider z1 being set  such that
A5: z1 in the carrier of X and
A6: z1 in Ball (x,r) and
A7: u = T . z1 by A3, FUNCT_2:64;
reconsider zz1 = z1 as Point of X by A5;
reconsider za1 = zz1 as Point of (LinearTopSpaceNorm X) by NORMSP_2:def_4;
consider z2 being set  such that
A8: z2 in the carrier of X and
A9: z2 in Ball (x,r) and
A10: v = T . z2 by A4, FUNCT_2:64;
reconsider zz2 = z2 as Point of X by A8;
A11: (1 - s) * v = T . ((1 - s) * zz2) by A10, LOPBAN_1:def_5;
reconsider za2 = zz2 as Point of (LinearTopSpaceNorm X) by NORMSP_2:def_4;
 ( s * za1 = s * zz1 & (1 - s) * za2 = (1 - s) * zz2 ) by NORMSP_2:def_4;
then A12: (s * za1) + ((1 - s) * za2) = (s * zz1) + ((1 - s) * zz2) by NORMSP_2:def_4;
 s * u = T . (s * zz1) by A7, LOPBAN_1:def_5;
then A13: (s * u) + ((1 - s) * v) = T . ((s * zz1) + ((1 - s) * zz2)) by A11, VECTSP_1:def_20;
 Bxr is convex by Th12;
then  (s * za1) + ((1 - s) * za2) in Bxr by A2, A6, A9, CONVEX1:def_2;
hence  (s * u) + ((1 - s) * v) in V1 by A12, A13, FUNCT_2:35; ::_thesis: verum
end;
assume A14: V = T .: (Ball (x,r)) ; ::_thesis: V is convex
 for u, v being Point of (LinearTopSpaceNorm Y)
for s being Real st 0 < s & s < 1 & u in V & v in V holds
(s * u) + ((1 - s) * v) in V
proof
let u, v be Point of (LinearTopSpaceNorm Y); ::_thesis: for s being Real st 0 < s & s < 1 & u in V & v in V holds
(s * u) + ((1 - s) * v) in V
let s be Real; ::_thesis: ( 0 < s & s < 1 & u in V & v in V implies (s * u) + ((1 - s) * v) in V )
reconsider u1 = u as Point of Y by NORMSP_2:def_4;
reconsider v1 = v as Point of Y by NORMSP_2:def_4;
 ( s * u1 = s * u & (1 - s) * v1 = (1 - s) * v ) by NORMSP_2:def_4;
then A15: (s * u1) + ((1 - s) * v1) = (s * u) + ((1 - s) * v) by NORMSP_2:def_4;
assume  ( 0 < s & s < 1 & u in V & v in V ) ; ::_thesis: (s * u) + ((1 - s) * v) in V
hence  (s * u) + ((1 - s) * v) in V by A14, A1, A15; ::_thesis: verum
end;
hence  V is convex by CONVEX1:def_2; ::_thesis: verum
end;

theorem Th14: :: LOPBAN_6:14
for X being RealNormSpace
for x being Point of X
for r, s being real number st r <= s holds
Ball (x,r) c= Ball (x,s)
proof
let X be RealNormSpace; ::_thesis: for x being Point of X
for r, s being real number st r <= s holds
Ball (x,r) c= Ball (x,s)
let x be Point of X; ::_thesis: for r, s being real number st r <= s holds
Ball (x,r) c= Ball (x,s)
let r, s be real number ; ::_thesis: ( r <= s implies Ball (x,r) c= Ball (x,s) )
assume A1: r <= s ; ::_thesis: Ball (x,r) c= Ball (x,s)
 for u being Point of X st u in Ball (x,r) holds
u in Ball (x,s)
proof
let u be Point of X; ::_thesis: ( u in Ball (x,r) implies u in Ball (x,s) )
assume  u in Ball (x,r) ; ::_thesis: u in Ball (x,s)
then  ex uu1 being Point of X st
( u = uu1 & ||.(x - uu1).|| < r ) ;
then  ||.(x - u).|| + r < r + s by A1, XREAL_1:8;
then  ||.(x - u).|| < (r + s) - r by XREAL_1:20;
hence  u in Ball (x,s) ; ::_thesis: verum
end;
hence  Ball (x,r) c= Ball (x,s) by SUBSET_1:2; ::_thesis: verum
end;

theorem Th15: :: LOPBAN_6:15
for X being RealBanachSpace
for Y being RealNormSpace
for T being Lipschitzian LinearOperator of X,Y
for r being real number
for BX1 being Subset of (LinearTopSpaceNorm X)
for TBX1, BYr being Subset of (LinearTopSpaceNorm Y) st r > 0 & BYr = Ball ((0. Y),r) & TBX1 = T .: (Ball ((0. X),1)) & BYr c= Cl TBX1 holds
BYr c= TBX1
proof
let X be RealBanachSpace; ::_thesis: for Y being RealNormSpace
for T being Lipschitzian LinearOperator of X,Y
for r being real number
for BX1 being Subset of (LinearTopSpaceNorm X)
for TBX1, BYr being Subset of (LinearTopSpaceNorm Y) st r > 0 & BYr = Ball ((0. Y),r) & TBX1 = T .: (Ball ((0. X),1)) & BYr c= Cl TBX1 holds
BYr c= TBX1
let Y be RealNormSpace; ::_thesis: for T being Lipschitzian LinearOperator of X,Y
for r being real number
for BX1 being Subset of (LinearTopSpaceNorm X)
for TBX1, BYr being Subset of (LinearTopSpaceNorm Y) st r > 0 & BYr = Ball ((0. Y),r) & TBX1 = T .: (Ball ((0. X),1)) & BYr c= Cl TBX1 holds
BYr c= TBX1
let T be Lipschitzian LinearOperator of X,Y; ::_thesis: for r being real number
for BX1 being Subset of (LinearTopSpaceNorm X)
for TBX1, BYr being Subset of (LinearTopSpaceNorm Y) st r > 0 & BYr = Ball ((0. Y),r) & TBX1 = T .: (Ball ((0. X),1)) & BYr c= Cl TBX1 holds
BYr c= TBX1
let r be real number ; ::_thesis: for BX1 being Subset of (LinearTopSpaceNorm X)
for TBX1, BYr being Subset of (LinearTopSpaceNorm Y) st r > 0 & BYr = Ball ((0. Y),r) & TBX1 = T .: (Ball ((0. X),1)) & BYr c= Cl TBX1 holds
BYr c= TBX1
let BX1 be Subset of (LinearTopSpaceNorm X); ::_thesis: for TBX1, BYr being Subset of (LinearTopSpaceNorm Y) st r > 0 & BYr = Ball ((0. Y),r) & TBX1 = T .: (Ball ((0. X),1)) & BYr c= Cl TBX1 holds
BYr c= TBX1
let TBX1, BYr be Subset of (LinearTopSpaceNorm Y); ::_thesis: ( r > 0 & BYr = Ball ((0. Y),r) & TBX1 = T .: (Ball ((0. X),1)) & BYr c= Cl TBX1 implies BYr c= TBX1 )
assume that
A1: r > 0 and
A2: BYr = Ball ((0. Y),r) and
A3: TBX1 = T .: (Ball ((0. X),1)) and
A4: BYr c= Cl TBX1 ; ::_thesis: BYr c= TBX1
A5: for x being Point of X
for y being Point of Y
for TB1, BYsr being Subset of (LinearTopSpaceNorm Y)
for s being real number st s > 0 & TB1 = T .: (Ball (x,s)) & y = T . x & BYsr = Ball (y,(s * r)) holds
BYsr c= Cl TB1
proof
reconsider TB01 = T .: (Ball ((0. X),1)) as Subset of Y ;
let x be Point of X; ::_thesis: for y being Point of Y
for TB1, BYsr being Subset of (LinearTopSpaceNorm Y)
for s being real number st s > 0 & TB1 = T .: (Ball (x,s)) & y = T . x & BYsr = Ball (y,(s * r)) holds
BYsr c= Cl TB1
let y be Point of Y; ::_thesis: for TB1, BYsr being Subset of (LinearTopSpaceNorm Y)
for s being real number st s > 0 & TB1 = T .: (Ball (x,s)) & y = T . x & BYsr = Ball (y,(s * r)) holds
BYsr c= Cl TB1
let TB1, BYsr be Subset of (LinearTopSpaceNorm Y); ::_thesis: for s being real number st s > 0 & TB1 = T .: (Ball (x,s)) & y = T . x & BYsr = Ball (y,(s * r)) holds
BYsr c= Cl TB1
let s be real number ; ::_thesis: ( s > 0 & TB1 = T .: (Ball (x,s)) & y = T . x & BYsr = Ball (y,(s * r)) implies BYsr c= Cl TB1 )
assume that
A6: s > 0 and
A7: TB1 = T .: (Ball (x,s)) and
A8: y = T . x and
A9: BYsr = Ball (y,(s * r)) ; ::_thesis: BYsr c= Cl TB1
reconsider s1 = s as non zero Real by A6, XREAL_0:def_1;
reconsider y1 = y as Point of (LinearTopSpaceNorm Y) by NORMSP_2:def_4;
A10: Ball (y,(s * r)) = y + (Ball ((0. Y),(s * r))) by Th2;
reconsider TB0xs = T .: (Ball (x,s)) as Subset of Y ;
reconsider TB0s = T .: (Ball ((0. X),s)) as Subset of Y ;
 Ball (x,s) = x + (Ball ((0. X),s)) by Th2;
then A11: y + TB0s = TB0xs by A8, Th6;
 s1 * BYr c= s1 * (Cl TBX1) by A4, CONVEX1:39;
then  s1 * BYr c= Cl (s1 * TBX1) by RLTOPSP1:52;
then  y1 + (s1 * BYr) c= y1 + (Cl (s1 * TBX1)) by RLTOPSP1:8;
then A12: y1 + (s1 * BYr) c= Cl (y1 + (s1 * TBX1)) by RLTOPSP1:38;
 Ball ((0. Y),(s * r)) = s1 * (Ball ((0. Y),r)) by A6, Th3;
then  Ball ((0. Y),(s * r)) = s1 * BYr by A2, Th9;
then A13: y1 + (s1 * BYr) = BYsr by A9, A10, Th8;
A14: s1 * (Ball ((0. X),1)) = Ball ((0. X),(s1 * 1)) by A6, Th3;
 s1 * TB01 = s1 * TBX1 by A3, Th9;
hence  BYsr c= Cl TB1 by A7, A12, A13, A11, A14, Th5, Th8; ::_thesis: verum
end;
A15: for s0 being real number st s0 > 0 holds
Ball ((0. Y),r) c= T .: (Ball ((0. X),(1 + s0)))
proof
let s0 be real number ; ::_thesis: ( s0 > 0 implies Ball ((0. Y),r) c= T .: (Ball ((0. X),(1 + s0))) )
assume A16: s0 > 0 ; ::_thesis: Ball ((0. Y),r) c= T .: (Ball ((0. X),(1 + s0)))
now__::_thesis:_for_z_being_set_st_z_in_Ball_((0._Y),r)_holds_
z_in_T_.:_(Ball_((0._X),(1_+_s0)))
let z be set ; ::_thesis: ( z in Ball ((0. Y),r) implies z in T .: (Ball ((0. X),(1 + s0))) )
assume A17: z in Ball ((0. Y),r) ; ::_thesis: z in T .: (Ball ((0. X),(1 + s0)))
then reconsider y = z as Point of Y ;
consider s1 being real number  such that
A18: 0 < s1 and
A19: s1 < s0 by A16, XREAL_1:5;
set a = s1 / (1 + s1);
set e = (s1 / (1 + s1)) GeoSeq ;
A20: s1 / (1 + s1) < 1 by A18, XREAL_1:29, XREAL_1:191;
then A21: abs (s1 / (1 + s1)) < 1 by A18, ABSVALUE:def_1;
then A22: (s1 / (1 + s1)) GeoSeq is summable by SERIES_1:24;
defpred S1[ Element of NAT , Point of X, Point of X, Point of X] means ( $3 in Ball ($2,(((s1 / (1 + s1)) GeoSeq) . $1)) & ||.((T . $3) - y).|| < (((s1 / (1 + s1)) GeoSeq) . ($1 + 1)) * r implies ( $4 in Ball ($3,(((s1 / (1 + s1)) GeoSeq) . ($1 + 1))) & ||.((T . $4) - y).|| < (((s1 / (1 + s1)) GeoSeq) . ($1 + 2)) * r ) );
reconsider B0 = Ball (y,((((s1 / (1 + s1)) GeoSeq) . 1) * r)) as Subset of (LinearTopSpaceNorm Y) by NORMSP_2:def_4;
A23: 0 < s1 / (1 + s1) by A18, XREAL_1:139;
then  ( ((s1 / (1 + s1)) GeoSeq) . 1 = (s1 / (1 + s1)) |^ 1 & 0 < (s1 / (1 + s1)) |^ 1 ) by NEWTON:83, PREPOWER:def_1;
then  0 < (((s1 / (1 + s1)) GeoSeq) . 1) * r by A1, XREAL_1:129;
then  ||.(y - y).|| < (((s1 / (1 + s1)) GeoSeq) . 1) * r by NORMSP_1:6;
then  ( B0 is open & y in B0 ) by NORMSP_2:23;
then  Ball (y,((((s1 / (1 + s1)) GeoSeq) . 1) * r)) meets TBX1 by A2, A4, A17, PRE_TOPC:def_7;
then consider s being set  such that
A24: s in Ball (y,((((s1 / (1 + s1)) GeoSeq) . 1) * r)) and
A25: s in T .: (Ball ((0. X),1)) by A3, XBOOLE_0:3;
consider xn1 being set  such that
A26: xn1 in the carrier of X and
A27: xn1 in Ball ((0. X),1) and
A28: s = T . xn1 by A25, FUNCT_2:64;
reconsider xn1 = xn1 as Point of X by A26;
A29: for n being Element of NAT
for v, w being Point of X ex z being Point of X st S1[n,v,w,z]
proof
let n be Element of NAT ; ::_thesis: for v, w being Point of X ex z being Point of X st S1[n,v,w,z]
let v, w be Point of X; ::_thesis: ex z being Point of X st S1[n,v,w,z]
now__::_thesis:_(_w_in_Ball_(v,(((s1_/_(1_+_s1))_GeoSeq)_._n))_&_||.((T_._w)_-_y).||_<_(((s1_/_(1_+_s1))_GeoSeq)_._(n_+_1))_*_r_implies_ex_z_being_Point_of_X_st_
(_z_in_Ball_(w,(((s1_/_(1_+_s1))_GeoSeq)_._(n_+_1)))_&_||.((T_._z)_-_y).||_<_(((s1_/_(1_+_s1))_GeoSeq)_._(n_+_2))_*_r_)_)
reconsider B0 = Ball (y,((((s1 / (1 + s1)) GeoSeq) . (n + 2)) * r)) as Subset of (LinearTopSpaceNorm Y) by NORMSP_2:def_4;
reconsider BYsr = Ball ((T . w),((((s1 / (1 + s1)) GeoSeq) . (n + 1)) * r)) as Subset of (LinearTopSpaceNorm Y) by NORMSP_2:def_4;
reconsider TB1 = T .: (Ball (w,(((s1 / (1 + s1)) GeoSeq) . (n + 1)))) as Subset of (LinearTopSpaceNorm Y) by NORMSP_2:def_4;
assume that
 w in Ball (v,(((s1 / (1 + s1)) GeoSeq) . n)) and
A30: ||.((T . w) - y).|| < (((s1 / (1 + s1)) GeoSeq) . (n + 1)) * r ; ::_thesis: ex z being Point of X st
( z in Ball (w,(((s1 / (1 + s1)) GeoSeq) . (n + 1))) & ||.((T . z) - y).|| < (((s1 / (1 + s1)) GeoSeq) . (n + 2)) * r )
 ((s1 / (1 + s1)) GeoSeq) . (n + 1) = (s1 / (1 + s1)) |^ (n + 1) by PREPOWER:def_1;
then A31: BYsr c= Cl TB1 by A5, A23, NEWTON:83;
 ( ((s1 / (1 + s1)) GeoSeq) . (n + 2) = (s1 / (1 + s1)) |^ (n + 2) & 0 < (s1 / (1 + s1)) |^ (n + 2) ) by A23, NEWTON:83, PREPOWER:def_1;
then  0 < (((s1 / (1 + s1)) GeoSeq) . (n + 2)) * r by A1, XREAL_1:129;
then  ||.(y - y).|| < (((s1 / (1 + s1)) GeoSeq) . (n + 2)) * r by NORMSP_1:6;
then A32: ( B0 is open & y in B0 ) by NORMSP_2:23;
 y in BYsr by A30;
then  Ball (y,((((s1 / (1 + s1)) GeoSeq) . (n + 2)) * r)) meets TB1 by A31, A32, PRE_TOPC:def_7;
then consider s being set  such that
A33: s in Ball (y,((((s1 / (1 + s1)) GeoSeq) . (n + 2)) * r)) and
A34: s in T .: (Ball (w,(((s1 / (1 + s1)) GeoSeq) . (n + 1)))) by XBOOLE_0:3;
consider z being set  such that
A35: z in the carrier of X and
A36: z in Ball (w,(((s1 / (1 + s1)) GeoSeq) . (n + 1))) and
A37: s = T . z by A34, FUNCT_2:64;
reconsider z = z as Point of X by A35;
reconsider sb = T . z as Point of Y ;
 ex ss1 being Point of Y st
( sb = ss1 & ||.(y - ss1).|| < (((s1 / (1 + s1)) GeoSeq) . (n + 2)) * r ) by A33, A37;
then  ||.((T . z) - y).|| < (((s1 / (1 + s1)) GeoSeq) . (n + 2)) * r by NORMSP_1:7;
hence  ex z being Point of X st
( z in Ball (w,(((s1 / (1 + s1)) GeoSeq) . (n + 1))) & ||.((T . z) - y).|| < (((s1 / (1 + s1)) GeoSeq) . (n + 2)) * r ) by A36; ::_thesis: verum
end;
hence  ex z being Point of X st S1[n,v,w,z] ; ::_thesis: verum
end;
consider xn being sequence of X such that
A38: ( xn . 0 = 0. X & xn . 1 = xn1 & ( for n being Element of NAT holds S1[n,xn . n,xn . (n + 1),xn . (n + 2)] ) ) from LOPBAN_6:sch_1(A29);
reconsider sb = T . xn1 as Point of Y ;
A39: ex ss1 being Point of Y st
( sb = ss1 & ||.(y - ss1).|| < (((s1 / (1 + s1)) GeoSeq) . 1) * r ) by A24, A28;
A40: for n being Element of NAT holds
( xn . (n + 1) in Ball ((xn . n),(((s1 / (1 + s1)) GeoSeq) . n)) & ||.((T . (xn . (n + 1))) - y).|| < (((s1 / (1 + s1)) GeoSeq) . (n + 1)) * r )
proof
defpred S2[ Element of NAT ] means ( xn . ($1 + 1) in Ball ((xn . $1),(((s1 / (1 + s1)) GeoSeq) . $1)) & ||.((T . (xn . ($1 + 1))) - y).|| < (((s1 / (1 + s1)) GeoSeq) . ($1 + 1)) * r );
A41: now__::_thesis:_for_n_being_Element_of_NAT_st_S2[n]_holds_
S2[n_+_1]
let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A42: S2[n] ; ::_thesis: S2[n + 1]
 S1[n,xn . n,xn . (n + 1),xn . (n + 2)] by A38;
hence  S2[n + 1] by A42; ::_thesis: verum
end;
A43: S2[ 0 ] by A27, A39, A38, NORMSP_1:7, PREPOWER:3;
thus  for n being Element of NAT holds S2[n] from NAT_1:sch_1(A43, A41); ::_thesis: verum
end;
A44: ((s1 / (1 + s1)) GeoSeq) . 0 = 1 by PREPOWER:3;
A45: for m, k being Element of NAT holds ||.((xn . (m + k)) - (xn . m)).|| <= (((s1 / (1 + s1)) GeoSeq) . m) * ((1 - (((s1 / (1 + s1)) GeoSeq) . k)) / (1 - (((s1 / (1 + s1)) GeoSeq) . 1)))
proof
let m be Element of NAT ; ::_thesis: for k being Element of NAT holds ||.((xn . (m + k)) - (xn . m)).|| <= (((s1 / (1 + s1)) GeoSeq) . m) * ((1 - (((s1 / (1 + s1)) GeoSeq) . k)) / (1 - (((s1 / (1 + s1)) GeoSeq) . 1)))
defpred S2[ Element of NAT ] means ||.((xn . (m + $1)) - (xn . m)).|| <= (((s1 / (1 + s1)) GeoSeq) . m) * ((1 - (((s1 / (1 + s1)) GeoSeq) . $1)) / (1 - (((s1 / (1 + s1)) GeoSeq) . 1)));
A46: now__::_thesis:_for_k_being_Element_of_NAT_st_S2[k]_holds_
S2[k_+_1]
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
A47: ((((s1 / (1 + s1)) |^ k) - ((s1 / (1 + s1)) |^ (k + 1))) / (1 - ((s1 / (1 + s1)) |^ 1))) + ((1 - ((s1 / (1 + s1)) |^ k)) / (1 - ((s1 / (1 + s1)) |^ 1))) = ((((s1 / (1 + s1)) |^ k) - ((s1 / (1 + s1)) |^ (k + 1))) + (1 - ((s1 / (1 + s1)) |^ k))) / (1 - ((s1 / (1 + s1)) |^ 1)) by XCMPLX_1:62
.= (1 - ((s1 / (1 + s1)) |^ (k + 1))) / (1 - ((s1 / (1 + s1)) |^ 1)) ;
assume  S2[k] ; ::_thesis: S2[k + 1]
then  ( ||.((xn . ((m + k) + 1)) - (xn . m)).|| <= ||.((xn . ((m + k) + 1)) - (xn . (m + k))).|| + ||.((xn . (m + k)) - (xn . m)).|| & ||.((xn . ((m + k) + 1)) - (xn . (m + k))).|| + ||.((xn . (m + k)) - (xn . m)).|| <= ||.((xn . ((m + k) + 1)) - (xn . (m + k))).|| + ((((s1 / (1 + s1)) GeoSeq) . m) * ((1 - (((s1 / (1 + s1)) GeoSeq) . k)) / (1 - (((s1 / (1 + s1)) GeoSeq) . 1)))) ) by NORMSP_1:10, XREAL_1:6;
then A48: ||.((xn . (m + (k + 1))) - (xn . m)).|| <= ||.((xn . ((m + k) + 1)) - (xn . (m + k))).|| + ((((s1 / (1 + s1)) GeoSeq) . m) * ((1 - (((s1 / (1 + s1)) GeoSeq) . k)) / (1 - (((s1 / (1 + s1)) GeoSeq) . 1)))) by XXREAL_0:2;
 xn . ((m + k) + 1) in Ball ((xn . (m + k)),(((s1 / (1 + s1)) GeoSeq) . (m + k))) by A40;
then  ex xn2 being Point of X st
( xn . ((m + k) + 1) = xn2 & ||.((xn . (m + k)) - xn2).|| < ((s1 / (1 + s1)) GeoSeq) . (m + k) ) ;
then  ||.((xn . ((m + k) + 1)) - (xn . (m + k))).|| < ((s1 / (1 + s1)) GeoSeq) . (m + k) by NORMSP_1:7;
then A49: ||.((xn . ((m + k) + 1)) - (xn . (m + k))).|| + ((((s1 / (1 + s1)) GeoSeq) . m) * ((1 - (((s1 / (1 + s1)) GeoSeq) . k)) / (1 - (((s1 / (1 + s1)) GeoSeq) . 1)))) <= (((s1 / (1 + s1)) GeoSeq) . (m + k)) + ((((s1 / (1 + s1)) GeoSeq) . m) * ((1 - (((s1 / (1 + s1)) GeoSeq) . k)) / (1 - (((s1 / (1 + s1)) GeoSeq) . 1)))) by XREAL_1:6;
 (s1 / (1 + s1)) |^ 1 < 1 by A20, NEWTON:5;
then  0 < 1 - ((s1 / (1 + s1)) |^ 1) by XREAL_1:50;
then A50: (s1 / (1 + s1)) |^ k = (((s1 / (1 + s1)) |^ k) * (1 - ((s1 / (1 + s1)) |^ 1))) / (1 - ((s1 / (1 + s1)) |^ 1)) by XCMPLX_1:89
.= (((s1 / (1 + s1)) |^ k) - (((s1 / (1 + s1)) |^ k) * ((s1 / (1 + s1)) |^ 1))) / (1 - ((s1 / (1 + s1)) |^ 1))
.= (((s1 / (1 + s1)) |^ k) - ((s1 / (1 + s1)) |^ (k + 1))) / (1 - ((s1 / (1 + s1)) |^ 1)) by NEWTON:8 ;
(((s1 / (1 + s1)) GeoSeq) . (m + k)) + ((((s1 / (1 + s1)) GeoSeq) . m) * ((1 - (((s1 / (1 + s1)) GeoSeq) . k)) / (1 - (((s1 / (1 + s1)) GeoSeq) . 1)))) = ((s1 / (1 + s1)) |^ (m + k)) + ((((s1 / (1 + s1)) GeoSeq) . m) * ((1 - (((s1 / (1 + s1)) GeoSeq) . k)) / (1 - (((s1 / (1 + s1)) GeoSeq) . 1)))) by PREPOWER:def_1
.= ((s1 / (1 + s1)) |^ (m + k)) + (((s1 / (1 + s1)) |^ m) * ((1 - (((s1 / (1 + s1)) GeoSeq) . k)) / (1 - (((s1 / (1 + s1)) GeoSeq) . 1)))) by PREPOWER:def_1
.= ((s1 / (1 + s1)) |^ (m + k)) + (((s1 / (1 + s1)) |^ m) * ((1 - ((s1 / (1 + s1)) |^ k)) / (1 - (((s1 / (1 + s1)) GeoSeq) . 1)))) by PREPOWER:def_1
.= ((s1 / (1 + s1)) |^ (m + k)) + (((s1 / (1 + s1)) |^ m) * ((1 - ((s1 / (1 + s1)) |^ k)) / (1 - ((s1 / (1 + s1)) |^ 1)))) by PREPOWER:def_1
.= (((s1 / (1 + s1)) |^ m) * ((s1 / (1 + s1)) |^ k)) + (((s1 / (1 + s1)) |^ m) * ((1 - ((s1 / (1 + s1)) |^ k)) / (1 - ((s1 / (1 + s1)) |^ 1)))) by NEWTON:8
.= ((s1 / (1 + s1)) |^ m) * ((1 - ((s1 / (1 + s1)) |^ (k + 1))) / (1 - ((s1 / (1 + s1)) |^ 1))) by A50, A47
.= (((s1 / (1 + s1)) GeoSeq) . m) * ((1 - ((s1 / (1 + s1)) |^ (k + 1))) / (1 - ((s1 / (1 + s1)) |^ 1))) by PREPOWER:def_1
.= (((s1 / (1 + s1)) GeoSeq) . m) * ((1 - (((s1 / (1 + s1)) GeoSeq) . (k + 1))) / (1 - ((s1 / (1 + s1)) |^ 1))) by PREPOWER:def_1
.= (((s1 / (1 + s1)) GeoSeq) . m) * ((1 - (((s1 / (1 + s1)) GeoSeq) . (k + 1))) / (1 - (((s1 / (1 + s1)) GeoSeq) . 1))) by PREPOWER:def_1 ;
hence  S2[k + 1] by A48, A49, XXREAL_0:2; ::_thesis: verum
end;
 ||.((xn . (m + 0)) - (xn . m)).|| = ||.(0. X).|| by RLVECT_1:5;
then A51: S2[ 0 ] by A44;
 for k being Element of NAT holds S2[k] from NAT_1:sch_1(A51, A46);
hence  for k being Element of NAT holds ||.((xn . (m + k)) - (xn . m)).|| <= (((s1 / (1 + s1)) GeoSeq) . m) * ((1 - (((s1 / (1 + s1)) GeoSeq) . k)) / (1 - (((s1 / (1 + s1)) GeoSeq) . 1))) ; ::_thesis: verum
end;
A52: for k being Element of NAT st 0 <= k holds
||.xn.|| . k <= 1 / (1 - (s1 / (1 + s1)))
proof
let k be Element of NAT ; ::_thesis: ( 0 <= k implies ||.xn.|| . k <= 1 / (1 - (s1 / (1 + s1))) )
assume  0 <= k ; ::_thesis: ||.xn.|| . k <= 1 / (1 - (s1 / (1 + s1)))
A53: ( ((s1 / (1 + s1)) GeoSeq) . k = (s1 / (1 + s1)) |^ k & ((s1 / (1 + s1)) GeoSeq) . 1 = (s1 / (1 + s1)) |^ 1 ) by PREPOWER:def_1;
 (s1 / (1 + s1)) |^ 1 < 1 by A20, NEWTON:5;
then A54: 0 < 1 - ((s1 / (1 + s1)) |^ 1) by XREAL_1:50;
 1 - ((s1 / (1 + s1)) |^ k) < 1 by A23, NEWTON:83, XREAL_1:44;
then  (1 - (((s1 / (1 + s1)) GeoSeq) . k)) / (1 - (((s1 / (1 + s1)) GeoSeq) . 1)) <= 1 / (1 - ((s1 / (1 + s1)) |^ 1)) by A53, A54, XREAL_1:74;
then A55: (1 - (((s1 / (1 + s1)) GeoSeq) . k)) / (1 - (((s1 / (1 + s1)) GeoSeq) . 1)) <= 1 / (1 - (s1 / (1 + s1))) by NEWTON:5;
 ||.((xn . (0 + k)) - (xn . 0)).|| <= (((s1 / (1 + s1)) GeoSeq) . 0) * ((1 - (((s1 / (1 + s1)) GeoSeq) . k)) / (1 - (((s1 / (1 + s1)) GeoSeq) . 1))) by A45;
then  ||.(xn . k).|| <= (1 - (((s1 / (1 + s1)) GeoSeq) . k)) / (1 - (((s1 / (1 + s1)) GeoSeq) . 1)) by A44, A38, RLVECT_1:13;
then  ||.(xn . k).|| <= 1 / (1 - (s1 / (1 + s1))) by A55, XXREAL_0:2;
hence  ||.xn.|| . k <= 1 / (1 - (s1 / (1 + s1))) by NORMSP_0:def_4; ::_thesis: verum
end;
A56: Sum ((s1 / (1 + s1)) GeoSeq) = 1 / (1 - (s1 / (1 + s1))) by A21, SERIES_1:24;
1 / (1 - (s1 / (1 + s1))) = 1 / (((1 * (1 + s1)) - s1) / (1 + s1)) by A18, XCMPLX_1:127
.= 1 + s1 by XCMPLX_1:100 ;
then A57: Sum ((s1 / (1 + s1)) GeoSeq) < 1 + s0 by A19, A56, XREAL_1:6;
set xx = lim xn;
A58: now__::_thesis:_for_m,_k_being_Element_of_NAT_holds_||.((xn_._(m_+_k))_-_(xn_._m)).||_<_((s1_/_(1_+_s1))_|^_m)_*_(1_/_(1_-_((s1_/_(1_+_s1))_|^_1)))
let m be Element of NAT ; ::_thesis: for k being Element of NAT holds ||.((xn . (m + k)) - (xn . m)).|| < ((s1 / (1 + s1)) |^ m) * (1 / (1 - ((s1 / (1 + s1)) |^ 1)))
hereby  ::_thesis: verum
let k be Element of NAT ; ::_thesis: ||.((xn . (m + k)) - (xn . m)).|| < ((s1 / (1 + s1)) |^ m) * (1 / (1 - ((s1 / (1 + s1)) |^ 1)))
A59: 0 < (s1 / (1 + s1)) |^ m by A23, NEWTON:83;
 ||.((xn . (m + k)) - (xn . m)).|| <= (((s1 / (1 + s1)) GeoSeq) . m) * ((1 - (((s1 / (1 + s1)) GeoSeq) . k)) / (1 - (((s1 / (1 + s1)) GeoSeq) . 1))) by A45;
then  ||.((xn . (m + k)) - (xn . m)).|| <= ((s1 / (1 + s1)) |^ m) * ((1 - (((s1 / (1 + s1)) GeoSeq) . k)) / (1 - (((s1 / (1 + s1)) GeoSeq) . 1))) by PREPOWER:def_1;
then  ||.((xn . (m + k)) - (xn . m)).|| <= ((s1 / (1 + s1)) |^ m) * ((1 - ((s1 / (1 + s1)) |^ k)) / (1 - (((s1 / (1 + s1)) GeoSeq) . 1))) by PREPOWER:def_1;
then A60: ||.((xn . (m + k)) - (xn . m)).|| <= ((s1 / (1 + s1)) |^ m) * ((1 - ((s1 / (1 + s1)) |^ k)) / (1 - ((s1 / (1 + s1)) |^ 1))) by PREPOWER:def_1;
 (s1 / (1 + s1)) |^ 1 < 1 by A20, NEWTON:5;
then A61: 0 < 1 - ((s1 / (1 + s1)) |^ 1) by XREAL_1:50;
 1 - ((s1 / (1 + s1)) |^ k) < 1 by A23, NEWTON:83, XREAL_1:44;
then  (1 - ((s1 / (1 + s1)) |^ k)) / (1 - ((s1 / (1 + s1)) |^ 1)) < 1 / (1 - ((s1 / (1 + s1)) |^ 1)) by A61, XREAL_1:74;
then  ((s1 / (1 + s1)) |^ m) * ((1 - ((s1 / (1 + s1)) |^ k)) / (1 - ((s1 / (1 + s1)) |^ 1))) < ((s1 / (1 + s1)) |^ m) * (1 / (1 - ((s1 / (1 + s1)) |^ 1))) by A59, XREAL_1:68;
hence  ||.((xn . (m + k)) - (xn . m)).|| < ((s1 / (1 + s1)) |^ m) * (1 / (1 - ((s1 / (1 + s1)) |^ 1))) by A60, XXREAL_0:2; ::_thesis: verum
end;
end;
now__::_thesis:_for_r1_being_Real_st_0_<_r1_holds_
ex_m_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_m_<=_n_holds_
||.((xn_._n)_-_(xn_._m)).||_<_r1
let r1 be Real; ::_thesis: ( 0 < r1 implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((xn . n) - (xn . m)).|| < r1 )
A62: ( (s1 / (1 + s1)) GeoSeq is convergent & lim ((s1 / (1 + s1)) GeoSeq) = 0 ) by A22, SERIES_1:4;
 (s1 / (1 + s1)) |^ 1 < 1 by A20, NEWTON:5;
then A63: 0 < 1 - ((s1 / (1 + s1)) |^ 1) by XREAL_1:50;
assume  0 < r1 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((xn . n) - (xn . m)).|| < r1
then  0 < r1 * (1 - ((s1 / (1 + s1)) |^ 1)) by A63, XREAL_1:129;
then consider p1 being Element of NAT  such that
A64: for m being Element of NAT st p1 <= m holds
abs ((((s1 / (1 + s1)) GeoSeq) . m) - 0) < r1 * (1 - ((s1 / (1 + s1)) |^ 1)) by A62, SEQ_2:def_7;
take m = p1; ::_thesis: for n being Element of NAT st m <= n holds
||.((xn . n) - (xn . m)).|| < r1
 abs ((((s1 / (1 + s1)) GeoSeq) . p1) - 0) < r1 * (1 - ((s1 / (1 + s1)) |^ 1)) by A64;
then  ((s1 / (1 + s1)) GeoSeq) . p1 < 0 + (r1 * (1 - ((s1 / (1 + s1)) |^ 1))) by RINFSUP1:1;
then  (((s1 / (1 + s1)) GeoSeq) . p1) / (1 - ((s1 / (1 + s1)) |^ 1)) < (r1 * (1 - ((s1 / (1 + s1)) |^ 1))) / (1 - ((s1 / (1 + s1)) |^ 1)) by A63, XREAL_1:74;
then  (((s1 / (1 + s1)) GeoSeq) . p1) / (1 - ((s1 / (1 + s1)) |^ 1)) < r1 by A63, XCMPLX_1:89;
then  ((s1 / (1 + s1)) |^ p1) / (1 - ((s1 / (1 + s1)) |^ 1)) < r1 by PREPOWER:def_1;
then A65: ((s1 / (1 + s1)) |^ p1) * (1 / (1 - ((s1 / (1 + s1)) |^ 1))) < r1 by XCMPLX_1:99;
hereby  ::_thesis: verum
let n be Element of NAT ; ::_thesis: ( m <= n implies ||.((xn . n) - (xn . m)).|| < r1 )
assume  m <= n ; ::_thesis: ||.((xn . n) - (xn . m)).|| < r1
then consider k1 being Nat such that
A66: n = m + k1 by NAT_1:10;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def_12;
 n = m + k1 by A66;
hence  ||.((xn . n) - (xn . m)).|| < r1 by A58, A65, XXREAL_0:2; ::_thesis: verum
end;
end;
then  xn is Cauchy_sequence_by_Norm by LOPBAN_3:5;
then A67: xn is convergent by LOPBAN_1:def_15;
then  lim ||.xn.|| = ||.(lim xn).|| by LOPBAN_1:41;
then  ||.(lim xn).|| <= Sum ((s1 / (1 + s1)) GeoSeq) by A56, A67, A52, LOPBAN_1:41, RSSPACE2:5;
then  ||.(lim xn).|| < 1 + s0 by A57, XXREAL_0:2;
then  ||.(- (lim xn)).|| < 1 + s0 by NORMSP_1:2;
then  ||.((0. X) - (lim xn)).|| < 1 + s0 by RLVECT_1:14;
then A68: lim xn in Ball ((0. X),(1 + s0)) ;
 rng xn c= the carrier of X ;
then A69: rng xn c= dom T by FUNCT_2:def_1;
A70: now__::_thesis:_for_n_being_Element_of_NAT_holds_(T_/*_xn)_._n_=_T_._(xn_._n)
let n be Element of NAT ; ::_thesis: (T /* xn) . n = T . (xn . n)
thus (T /* xn) . n = T /. (xn . n) by A69, FUNCT_2:109
.= T . (xn . n) ; ::_thesis: verum
end;
A71: now__::_thesis:_for_s_being_Real_st_0_<_s_holds_
ex_m_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_m_<=_n_holds_
||.(((T_/*_xn)_._n)_-_y).||_<_s
let s be Real; ::_thesis: ( 0 < s implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((T /* xn) . n) - y).|| < s )
assume  0 < s ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((T /* xn) . n) - y).|| < s
then A72: 0 < s / r by A1, XREAL_1:139;
 ( (s1 / (1 + s1)) GeoSeq is convergent & lim ((s1 / (1 + s1)) GeoSeq) = 0 ) by A22, SERIES_1:4;
then consider m0 being Element of NAT  such that
A73: for n being Element of NAT st m0 <= n holds
abs ((((s1 / (1 + s1)) GeoSeq) . n) - 0) < s / r by A72, SEQ_2:def_7;
take m = m0 + 1; ::_thesis: for n being Element of NAT st m <= n holds
||.(((T /* xn) . n) - y).|| < s
 ( (s1 / (1 + s1)) |^ 1 < 1 & 0 < (s1 / (1 + s1)) |^ m0 ) by A23, A20, NEWTON:5, NEWTON:83;
then  ((s1 / (1 + s1)) |^ m0) * ((s1 / (1 + s1)) |^ 1) <= (s1 / (1 + s1)) |^ m0 by XREAL_1:153;
then  (s1 / (1 + s1)) |^ (m0 + 1) <= (s1 / (1 + s1)) |^ m0 by NEWTON:8;
then  ((s1 / (1 + s1)) GeoSeq) . (m0 + 1) <= (s1 / (1 + s1)) |^ m0 by PREPOWER:def_1;
then A74: ((s1 / (1 + s1)) GeoSeq) . (m0 + 1) <= ((s1 / (1 + s1)) GeoSeq) . m0 by PREPOWER:def_1;
 abs ((((s1 / (1 + s1)) GeoSeq) . m0) - 0) < s / r by A73;
then  ((s1 / (1 + s1)) GeoSeq) . m0 < 0 + (s / r) by RINFSUP1:1;
then  ((s1 / (1 + s1)) GeoSeq) . (m0 + 1) < s / r by A74, XXREAL_0:2;
then  (((s1 / (1 + s1)) GeoSeq) . (m0 + 1)) * r < (s / r) * r by A1, XREAL_1:68;
then A75: (((s1 / (1 + s1)) GeoSeq) . (m0 + 1)) * r < s by A1, XCMPLX_1:87;
now__::_thesis:_for_n_being_Element_of_NAT_st_m_<=_n_holds_
||.(((T_/*_xn)_._n)_-_y).||_<_s
let n be Element of NAT ; ::_thesis: ( m <= n implies ||.(((T /* xn) . n) - y).|| < s )
assume A76: m <= n ; ::_thesis: ||.(((T /* xn) . n) - y).|| < s
 1 <= m0 + 1 by NAT_1:11;
then reconsider n0 = n - 1 as Element of NAT by A76, NAT_1:21, XXREAL_0:2;
consider m1 being Nat such that
A77: n0 + 1 = (m0 + 1) + m1 by A76, NAT_1:10;
A78: (s1 / (1 + s1)) |^ (n0 + 1) = ((s1 / (1 + s1)) |^ (m0 + 1)) * ((s1 / (1 + s1)) |^ m1) by A77, NEWTON:8;
A79: 1 |^ m1 = 1 by NEWTON:10;
 ( 0 < (s1 / (1 + s1)) |^ (m0 + 1) & (s1 / (1 + s1)) |^ m1 <= 1 |^ m1 ) by A23, A20, NEWTON:83, PREPOWER:9;
then  (s1 / (1 + s1)) |^ (n0 + 1) <= (s1 / (1 + s1)) |^ (m0 + 1) by A78, A79, XREAL_1:153;
then  ((s1 / (1 + s1)) GeoSeq) . (n0 + 1) <= (s1 / (1 + s1)) |^ (m0 + 1) by PREPOWER:def_1;
then  ((s1 / (1 + s1)) GeoSeq) . (n0 + 1) <= ((s1 / (1 + s1)) GeoSeq) . (m0 + 1) by PREPOWER:def_1;
then  (((s1 / (1 + s1)) GeoSeq) . (n0 + 1)) * r <= (((s1 / (1 + s1)) GeoSeq) . (m0 + 1)) * r by A1, XREAL_1:64;
then  ||.((T . (xn . n)) - y).|| <= (((s1 / (1 + s1)) GeoSeq) . (m0 + 1)) * r by A40, XXREAL_0:2;
then  ||.((T . (xn . n)) - y).|| < s by A75, XXREAL_0:2;
hence  ||.(((T /* xn) . n) - y).|| < s by A70; ::_thesis: verum
end;
hence  for n being Element of NAT st m <= n holds
||.(((T /* xn) . n) - y).|| < s ; ::_thesis: verum
end;
 T is_continuous_in lim xn by LOPBAN_5:4;
then  ( T /* xn is convergent & T /. (lim xn) = lim (T /* xn) ) by A67, A69, NFCONT_1:def_5;
then  y = T . (lim xn) by A71, NORMSP_1:def_7;
hence  z in T .: (Ball ((0. X),(1 + s0))) by A68, FUNCT_2:35; ::_thesis: verum
end;
hence  Ball ((0. Y),r) c= T .: (Ball ((0. X),(1 + s0))) by TARSKI:def_3; ::_thesis: verum
end;
now__::_thesis:_for_z_being_set_st_z_in_Ball_((0._Y),r)_holds_
z_in_T_.:_(Ball_((0._X),1))
reconsider TB01 = T .: (Ball ((0. X),1)) as Subset of Y ;
let z be set ; ::_thesis: ( z in Ball ((0. Y),r) implies z in T .: (Ball ((0. X),1)) )
assume A80: z in Ball ((0. Y),r) ; ::_thesis: z in T .: (Ball ((0. X),1))
then reconsider y = z as Point of Y ;
 ex yy1 being Point of Y st
( y = yy1 & ||.((0. Y) - yy1).|| < r ) by A80;
then  ||.(- y).|| < r by RLVECT_1:14;
then A81: ||.y.|| < r by NORMSP_1:2;
consider s0 being real number  such that
A82: 0 < s0 and
A83: ||.y.|| < r / (1 + s0) and
 r / (1 + s0) < r by A81, Th1;
set y1 = (1 + s0) * y;
 (1 + s0) * ||.y.|| < (r / (1 + s0)) * (1 + s0) by A82, A83, XREAL_1:68;
then  (1 + s0) * ||.y.|| < r by A82, XCMPLX_1:87;
then  (abs (1 + s0)) * ||.y.|| < r by A82, ABSVALUE:def_1;
then  ||.((1 + s0) * y).|| < r by NORMSP_1:def_1;
then  ||.(- ((1 + s0) * y)).|| < r by NORMSP_1:2;
then  ||.((0. Y) - ((1 + s0) * y)).|| < r by RLVECT_1:14;
then A84: (1 + s0) * y in Ball ((0. Y),r) ;
 Ball ((0. Y),r) c= T .: (Ball ((0. X),(1 + s0))) by A15, A82;
then A85: (1 + s0) * y in T .: (Ball ((0. X),(1 + s0))) by A84;
reconsider s1 = 1 + s0 as non zero Real by A82;
 s1 * (Ball ((0. X),1)) = Ball ((0. X),(s1 * 1)) by A82, Th3;
then  s1 * y in s1 * TB01 by A85, Th5;
then  (s1 ") * (s1 * y) in (s1 ") * (s1 * TB01) ;
then  ((s1 ") * s1) * y in (s1 ") * (s1 * TB01) by RLVECT_1:def_7;
then A86: ((s1 ") * s1) * y in ((s1 ") * s1) * TB01 by CONVEX1:37;
(s1 ") * s1 = (1 / s1) * s1 by XCMPLX_1:215
.= 1 by XCMPLX_1:106 ;
then  y in 1 * TB01 by A86, RLVECT_1:def_8;
hence  z in T .: (Ball ((0. X),1)) by CONVEX1:32; ::_thesis: verum
end;
hence  BYr c= TBX1 by A2, A3, TARSKI:def_3; ::_thesis: verum
end;

theorem :: LOPBAN_6:16
for X, Y being RealBanachSpace
for T being Lipschitzian LinearOperator of X,Y
for T1 being Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y) st T1 = T & T1 is onto holds
T1 is open
proof
let X, Y be RealBanachSpace; ::_thesis: for T being Lipschitzian LinearOperator of X,Y
for T1 being Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y) st T1 = T & T1 is onto holds
T1 is open
let T be Lipschitzian LinearOperator of X,Y; ::_thesis: for T1 being Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y) st T1 = T & T1 is onto holds
T1 is open
let T1 be Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y); ::_thesis: ( T1 = T & T1 is onto implies T1 is open )
assume that
A1: T1 = T and
A2: T1 is onto ; ::_thesis: T1 is open
thus  for G being Subset of (LinearTopSpaceNorm X) st G is open holds
T1 .: G is open :: according to T_0TOPSP:def_2 ::_thesis: verum
proof
reconsider TB1 = T .: (Ball ((0. X),1)) as Subset of (LinearTopSpaceNorm Y) by NORMSP_2:def_4;
defpred S1[ Element of NAT , set ] means  ex TBn being Subset of (TopSpaceNorm Y) st
( TBn = T .: (Ball ((0. X),$1)) & $2 = Cl TBn );
let G be Subset of (LinearTopSpaceNorm X); ::_thesis: ( G is open implies T1 .: G is open )
A3: for n being Element of NAT ex y being Element of bool the carrier of Y st S1[n,y]
proof
let n be Element of NAT ; ::_thesis: ex y being Element of bool the carrier of Y st S1[n,y]
reconsider TBn = T .: (Ball ((0. X),n)) as Subset of (TopSpaceNorm Y) ;
 Cl TBn c= the carrier of Y ;
hence  ex y being Element of bool the carrier of Y st S1[n,y] ; ::_thesis: verum
end;
consider f being Function of NAT,(bool the carrier of Y) such that
A4: for x being Element of NAT holds S1[x,f . x] from FUNCT_2:sch_3(A3);
reconsider f = f as SetSequence of Y ;
A5: for n being Element of NAT holds f . n is closed
proof
let n be Element of NAT ; ::_thesis: f . n is closed
 ex TBn being Subset of (TopSpaceNorm Y) st
( TBn = T .: (Ball ((0. X),n)) & f . n = Cl TBn ) by A4;
hence  f . n is closed by NORMSP_2:15; ::_thesis: verum
end;
A6: the carrier of Y c= union (rng f)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in the carrier of Y or z in union (rng f) )
assume  z in the carrier of Y ; ::_thesis: z in union (rng f)
then reconsider z1 = z as Point of Y ;
 rng T = the carrier of (LinearTopSpaceNorm Y) by A1, A2, FUNCT_2:def_3;
then  rng T = the carrier of Y by NORMSP_2:def_4;
then consider x1 being set  such that
A7: x1 in the carrier of X and
A8: z1 = T . x1 by FUNCT_2:11;
reconsider x1 = x1 as Point of X by A7;
consider m being Element of NAT  such that
A9: ||.x1.|| <= m by MESFUNC1:8;
set n = m + 1;
 ||.x1.|| + 0 < m + 1 by A9, XREAL_1:8;
then  ||.(- x1).|| < m + 1 by NORMSP_1:2;
then  ||.((0. X) - x1).|| < m + 1 by RLVECT_1:14;
then  x1 in Ball ((0. X),(m + 1)) ;
then A10: T . x1 in T .: (Ball ((0. X),(m + 1))) by FUNCT_2:35;
 NAT = dom f by FUNCT_2:def_1;
then A11: f . (m + 1) in rng f by FUNCT_1:3;
consider TBn being Subset of (TopSpaceNorm Y) such that
A12: TBn = T .: (Ball ((0. X),(m + 1))) and
A13: f . (m + 1) = Cl TBn by A4;
 TBn c= f . (m + 1) by A13, PRE_TOPC:18;
hence  z in union (rng f) by A8, A10, A12, A11, TARSKI:def_4; ::_thesis: verum
end;
 union (rng f) is Subset of Y by PROB_1:11;
then  union (rng f) = the carrier of Y by A6, XBOOLE_0:def_10;
then consider n0 being Element of NAT , r being Real, y0 being Point of Y such that
A14: 0 < r and
A15: Ball (y0,r) c= f . n0 by A5, LOPBAN_5:3;
consider TBn0 being Subset of (TopSpaceNorm Y) such that
A16: TBn0 = T .: (Ball ((0. X),n0)) and
A17: f . n0 = Cl TBn0 by A4;
consider TBn01 being Subset of (TopSpaceNorm Y) such that
A18: TBn01 = T .: (Ball ((0. X),(n0 + 1))) and
A19: f . (n0 + 1) = Cl TBn01 by A4;
 Ball ((0. X),n0) c= Ball ((0. X),(n0 + 1)) by Th14, NAT_1:11;
then  TBn0 c= TBn01 by A16, A18, RELAT_1:123;
then  f . n0 c= f . (n0 + 1) by A17, A19, PRE_TOPC:19;
then A20: Ball (y0,r) c= Cl TBn01 by A15, A19, XBOOLE_1:1;
reconsider LTBn01 = TBn01 as Subset of (LinearTopSpaceNorm Y) by NORMSP_2:def_4;
 - 1 is non zero Real ;
then A21: Cl ((- 1) * LTBn01) = (- 1) * (Cl LTBn01) by RLTOPSP1:52;
reconsider yy0 = y0 as Point of (LinearTopSpaceNorm Y) by NORMSP_2:def_4;
A22: Ball ((0. Y),(r / ((2 * n0) + 2))) is Subset of (LinearTopSpaceNorm Y) by NORMSP_2:def_4;
 ||.(y0 - y0).|| < r by A14, NORMSP_1:6;
then  y0 in Ball (y0,r) ;
then  y0 in Cl TBn01 by A20;
then  yy0 in Cl LTBn01 by Th10;
then A23: (- 1) * yy0 in (- 1) * (Cl LTBn01) ;
reconsider nb1 = 1 / ((2 * n0) + 2) as non zero Real by XREAL_1:139;
reconsider TBX1 = T .: (Ball ((0. X),1)) as Subset of Y ;
reconsider my0 = {(- yy0)} as Subset of (LinearTopSpaceNorm Y) ;
reconsider TBnx01 = T .: (Ball ((0. X),(n0 + 1))) as Subset of (LinearTopSpaceNorm Y) by NORMSP_2:def_4;
reconsider BYyr = Ball (y0,r) as Subset of (LinearTopSpaceNorm Y) by NORMSP_2:def_4;
reconsider BYr = Ball ((0. Y),r) as Subset of (LinearTopSpaceNorm Y) by NORMSP_2:def_4;
reconsider XTB01 = T .: (Ball ((0. X),(n0 + 1))) as Subset of Y ;
A24: - yy0 = (- 1) * yy0 by RLVECT_1:16
.= (- 1) * y0 by NORMSP_2:def_4
.= - y0 by RLVECT_1:16 ;
(- 1) * LTBn01 = (- 1) * XTB01 by A18, Th9
.= T .: ((- 1) * (Ball ((0. X),(n0 + 1)))) by Th5
.= LTBn01 by A18, Th11 ;
then  - yy0 in Cl LTBn01 by A21, A23, RLVECT_1:16;
then  - yy0 in Cl TBn01 by Th10;
then  {(- yy0)} c= Cl TBn01 by ZFMISC_1:31;
then A25: my0 c= Cl TBnx01 by A18, Th10;
 BYyr c= Cl TBnx01 by A18, A20, Th10;
then  my0 + BYyr c= (Cl TBnx01) + (Cl TBnx01) by A25, RLTOPSP1:11;
then  (- yy0) + BYyr c= (Cl TBnx01) + (Cl TBnx01) by RUSUB_4:33;
then A26: (- y0) + (Ball (y0,r)) c= (Cl TBnx01) + (Cl TBnx01) by A24, Th8;
A27: (Cl TBnx01) + (Cl TBnx01) c= Cl (TBnx01 + TBnx01) by RLTOPSP1:62;
 Ball (y0,r) = y0 + (Ball ((0. Y),r)) by Th2;
then  BYyr = yy0 + BYr by Th8;
then  (- yy0) + BYyr = ((- yy0) + yy0) + BYr by RLTOPSP1:6;
then  (- yy0) + BYyr = (0. (LinearTopSpaceNorm Y)) + BYr by RLVECT_1:5;
then  (- yy0) + BYyr = {(0. (LinearTopSpaceNorm Y))} + BYr by RUSUB_4:33;
then  (- yy0) + BYyr = BYr by CONVEX1:35;
then  Ball ((0. Y),r) = (- y0) + (Ball (y0,r)) by A24, Th8;
then A28: Ball ((0. Y),r) c= Cl (TBnx01 + TBnx01) by A26, A27, XBOOLE_1:1;
 TBnx01 = 1 * TBnx01 by CONVEX1:32;
then A29: TBnx01 + TBnx01 = (1 + 1) * TBnx01 by Th13, CONVEX1:13
.= 2 * TBnx01 ;
 Ball ((0. X),((n0 + 1) * 1)) = (n0 + 1) * (Ball ((0. X),1)) by Th3;
then  (n0 + 1) * TBX1 = T .: (Ball ((0. X),(n0 + 1))) by Th5;
then TBnx01 + TBnx01 = 2 * ((n0 + 1) * TB1) by A29, Th9
.= (2 * (n0 + 1)) * TB1 by CONVEX1:37
.= ((2 * n0) + 2) * TB1 ;
then A30: Cl (TBnx01 + TBnx01) = ((2 * n0) + 2) * (Cl TB1) by RLTOPSP1:52;
A31: 0 < r / ((2 * n0) + 2) by A14, XREAL_1:139;
Ball ((0. Y),(r / ((2 * n0) + 2))) = Ball ((0. Y),((r * 1) / ((2 * n0) + 2)))
.= Ball ((0. Y),(r * (1 / ((2 * n0) + 2)))) by XCMPLX_1:74
.= nb1 * (Ball ((0. Y),r)) by Th3
.= nb1 * BYr by Th9 ;
then A32: Ball ((0. Y),(r / ((2 * n0) + 2))) c= (1 / ((2 * n0) + 2)) * (((2 * n0) + 2) * (Cl TB1)) by A28, A30, CONVEX1:39;
(1 / ((2 * n0) + 2)) * (((2 * n0) + 2) * (Cl TB1)) = ((1 / ((2 * n0) + 2)) * ((2 * n0) + 2)) * (Cl TB1) by CONVEX1:37
.= 1 * (Cl TB1) by XCMPLX_1:106
.= Cl TB1 by CONVEX1:32 ;
then A33: Ball ((0. Y),(r / ((2 * n0) + 2))) c= T .: (Ball ((0. X),1)) by A14, A32, A22, Th15, XREAL_1:139;
A34: for p being Real st p > 0 holds
ex q being Real st
( 0 < q & Ball ((0. Y),q) c= T .: (Ball ((0. X),p)) )
proof
reconsider TB1 = T .: (Ball ((0. X),1)) as Subset of Y ;
let p be Real; ::_thesis: ( p > 0 implies ex q being Real st
( 0 < q & Ball ((0. Y),q) c= T .: (Ball ((0. X),p)) ) )
assume A35: p > 0 ; ::_thesis: ex q being Real st
( 0 < q & Ball ((0. Y),q) c= T .: (Ball ((0. X),p)) )
then A36: p * (Ball ((0. X),1)) = Ball ((0. X),(p * 1)) by Th3;
take  (r / ((2 * n0) + 2)) * p ; ::_thesis: ( 0 < (r / ((2 * n0) + 2)) * p & Ball ((0. Y),((r / ((2 * n0) + 2)) * p)) c= T .: (Ball ((0. X),p)) )
 p * (Ball ((0. Y),(r / ((2 * n0) + 2)))) c= p * TB1 by A33, CONVEX1:39;
then  Ball ((0. Y),((r / ((2 * n0) + 2)) * p)) c= p * TB1 by A35, Th3;
hence  ( 0 < (r / ((2 * n0) + 2)) * p & Ball ((0. Y),((r / ((2 * n0) + 2)) * p)) c= T .: (Ball ((0. X),p)) ) by A31, A35, A36, Th5, XREAL_1:129; ::_thesis: verum
end;
assume A37: G is open ; ::_thesis: T1 .: G is open
now__::_thesis:_for_y_being_Point_of_Y_st_y_in_T1_.:_G_holds_
ex_q_being_Real_st_
(_0_<_q_&__{__w_where_w_is_Point_of_Y_:_||.(y_-_w).||_<_q__}__c=_T1_.:_G_)
let y be Point of Y; ::_thesis: ( y in T1 .: G implies ex q being Real st
( 0 < q &  {  w where w is Point of Y : ||.(y - w).|| < q  }  c= T1 .: G ) )
assume  y in T1 .: G ; ::_thesis: ex q being Real st
( 0 < q &  {  w where w is Point of Y : ||.(y - w).|| < q  }  c= T1 .: G )
then consider x being Point of X such that
A38: x in G and
A39: y = T . x by A1, FUNCT_2:65;
consider p being Real such that
A40: p > 0 and
A41:  {  z where z is Point of X : ||.(x - z).|| < p  }  c= G by A37, A38, NORMSP_2:22;
reconsider TBp = T .: (Ball ((0. X),p)) as Subset of Y ;
consider q being Real such that
A42: 0 < q and
A43: Ball ((0. Y),q) c= TBp by A34, A40;
 Ball (x,p) c= G by A41;
then A44: x + (Ball ((0. X),p)) c= G by Th2;
now__::_thesis:_for_t_being_set_st_t_in_y_+_TBp_holds_
t_in_T1_.:_G
let t be set ; ::_thesis: ( t in y + TBp implies t in T1 .: G )
assume  t in y + TBp ; ::_thesis: t in T1 .: G
then consider tz0 being Point of Y such that
A45: t = y + tz0 and
A46: tz0 in TBp ;
consider z0 being Element of X such that
A47: z0 in Ball ((0. X),p) and
A48: tz0 = T . z0 by A46, FUNCT_2:65;
reconsider z0 = z0 as Point of X ;
A49: x + z0 in x + (Ball ((0. X),p)) by A47;
 t = T . (x + z0) by A39, A45, A48, VECTSP_1:def_20;
hence  t in T1 .: G by A1, A44, A49, FUNCT_2:35; ::_thesis: verum
end;
then A50: y + TBp c= T .: G by A1, TARSKI:def_3;
take q = q; ::_thesis: ( 0 < q &  {  w where w is Point of Y : ||.(y - w).|| < q  }  c= T1 .: G )
now__::_thesis:_for_t_being_set_st_t_in_y_+_(Ball_((0._Y),q))_holds_
t_in_y_+_TBp
let t be set ; ::_thesis: ( t in y + (Ball ((0. Y),q)) implies t in y + TBp )
assume  t in y + (Ball ((0. Y),q)) ; ::_thesis: t in y + TBp
then  ex z0 being Point of Y st
( t = y + z0 & z0 in Ball ((0. Y),q) ) ;
hence  t in y + TBp by A43; ::_thesis: verum
end;
then  y + (Ball ((0. Y),q)) c= y + TBp by TARSKI:def_3;
then  Ball (y,q) c= y + TBp by Th2;
hence  ( 0 < q &  {  w where w is Point of Y : ||.(y - w).|| < q  }  c= T1 .: G ) by A1, A50, A42, XBOOLE_1:1; ::_thesis: verum
end;
hence  T1 .: G is open by NORMSP_2:22; ::_thesis: verum
end;
end;