:: 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;