let X be RealBanachSpace; :: thesis: for Y being RealNormSpace
for T being Lipschitzian LinearOperator of X,Y
for r being Real
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
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
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; :: 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 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 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 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 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; :: 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;
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 st s0 > 0 holds
Ball ((0. Y),r) c= T .: (Ball ((0. X),(1 + s0)))
proof
let s0 be Real; :: 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 object st z in Ball ((0. Y),r) holds
z in T .: (Ball ((0. X),(1 + s0)))
let z be object ; :: 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 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: |.(s1 / (1 + s1)).| < 1 by A18, ABSVALUE:def 1;
then A22: (s1 / (1 + s1)) GeoSeq is summable by SERIES_1:24;
defpred S1[ 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 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 object 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 object 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 Nat
for v, w being Point of X ex z being Point of X st S1[n,v,w,z]
proof
let n be 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 object 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 object 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 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 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[ 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 Nat st S2[n] holds
S2[n + 1]
let n be 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 Nat holds S2[n] from NAT_1:sch 2(A43, A41); :: thesis: verum
end;
A44: ((s1 / (1 + s1)) GeoSeq) . 0 = 1 by PREPOWER:3;
A45: for m, k being 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 Nat; :: thesis: for k being 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[ 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 Nat st S2[k] holds
S2[k + 1]
let k be 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;
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 Nat holds S2[k] from NAT_1:sch 2(A51, A46);
 hence for k being 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 Nat st 0 <= k holds
||.xn.|| . k <= 1 / (1 - (s1 / (1 + s1)))
proof
let k be 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;
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))) ;
||.((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 Nat holds ||.((xn . (m + k)) - (xn . m)).|| < ((s1 / (1 + s1)) |^ m) * (1 / (1 - ((s1 / (1 + s1)) |^ 1)))
let m be Nat; :: thesis: for k being Nat holds ||.((xn . (m + k)) - (xn . m)).|| < ((s1 / (1 + s1)) |^ m) * (1 / (1 - ((s1 / (1 + s1)) |^ 1)))
hereby :: thesis: verum
let k be 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;
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 Nat st
for n being Nat st m <= n holds
||.((xn . n) - (xn . m)).|| < r1
let r1 be Real; :: thesis: ( 0 < r1 implies ex m being Nat st
for n being 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;
then A63: 0 < 1 - ((s1 / (1 + s1)) |^ 1) by XREAL_1:50;
assume 0 < r1 ; :: thesis: ex m being Nat st
for n being 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 Nat such that
A64: for m being Nat st p1 <= m holds
|.((((s1 / (1 + s1)) GeoSeq) . m) - 0).| < r1 * (1 - ((s1 / (1 + s1)) |^ 1)) by A62, SEQ_2:def 7;
reconsider p1 = p1 as Nat ;
take m = p1; :: thesis: for n being Nat st m <= n holds
||.((xn . n) - (xn . m)).|| < r1
|.((((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 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 Nat ;
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 Nat holds (T /* xn) . n = T . (xn . n)
let n be Nat; :: thesis: (T /* xn) . n = T . (xn . n)
A71: n in NAT by ORDINAL1:def 12;
thus (T /* xn) . n = T /. (xn . n) by A69, FUNCT_2:109, A71
.= T . (xn . n) ; :: thesis: verum
end;
A72: now :: thesis: for s being Real st 0 < s holds
ex m being Nat st
for n being Nat st m <= n holds
||.(((T /* xn) . n) - y).|| < s
let s be Real; :: thesis: ( 0 < s implies ex m being Nat st
for n being Nat st m <= n holds
||.(((T /* xn) . n) - y).|| < s )
assume 0 < s ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
||.(((T /* xn) . n) - y).|| < s
then A73: 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 Nat such that
A74: for n being Nat st m0 <= n holds
|.((((s1 / (1 + s1)) GeoSeq) . n) - 0).| < s / r by A73, SEQ_2:def 7;
reconsider m = m0 + 1 as Nat ;
take m = m; :: thesis: for n being Nat st m <= n holds
||.(((T /* xn) . n) - y).|| < s
( (s1 / (1 + s1)) |^ 1 < 1 & 0 < (s1 / (1 + s1)) |^ m0 ) by A23, A20, 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 A75: ((s1 / (1 + s1)) GeoSeq) . (m0 + 1) <= ((s1 / (1 + s1)) GeoSeq) . m0 by PREPOWER:def 1;
|.((((s1 / (1 + s1)) GeoSeq) . m0) - 0).| < s / r by A74;
then ((s1 / (1 + s1)) GeoSeq) . m0 < 0 + (s / r) by RINFSUP1:1;
then ((s1 / (1 + s1)) GeoSeq) . (m0 + 1) < s / r by A75, XXREAL_0:2;
then (((s1 / (1 + s1)) GeoSeq) . (m0 + 1)) * r < (s / r) * r by A1, XREAL_1:68;
then A76: (((s1 / (1 + s1)) GeoSeq) . (m0 + 1)) * r < s by A1, XCMPLX_1:87;
now :: thesis: for n being Nat st m <= n holds
||.(((T /* xn) . n) - y).|| < s
let n be Nat; :: thesis: ( m <= n implies ||.(((T /* xn) . n) - y).|| < s )
assume A77: m <= n ; :: thesis: ||.(((T /* xn) . n) - y).|| < s
1 <= m0 + 1 by NAT_1:11;
then reconsider n0 = n - 1 as Nat by A77, NAT_1:21, XXREAL_0:2;
consider m1 being Nat such that
A78: n0 + 1 = (m0 + 1) + m1 by A77, NAT_1:10;
A79: (s1 / (1 + s1)) |^ (n0 + 1) = ((s1 / (1 + s1)) |^ (m0 + 1)) * ((s1 / (1 + s1)) |^ m1) by A78, NEWTON:8;
( 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 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 A76, XXREAL_0:2;
hence ||.(((T /* xn) . n) - y).|| < s by A70; :: thesis: verum
end;
hence for n being 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 A72, 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))) ; :: thesis: verum
end;
now :: thesis: for z being object 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 object ; :: 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 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 |.(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; :: thesis: verum