let X be RealBanachSpace; :: thesis: for X0 being Subset of (LinearTopSpaceNorm X)
for Y being RealBanachSpace
for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st X0 is dense & ( for x being Point of X st x in X0 holds
vseq # x is convergent ) & ( for x being Point of X ex K being Real st
( 0 <= K & ( for n being Nat holds ||.((vseq # x) . n).|| <= K ) ) ) holds
for x being Point of X holds vseq # x is convergent
let X0 be Subset of (LinearTopSpaceNorm X); :: thesis: for Y being RealBanachSpace
for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st X0 is dense & ( for x being Point of X st x in X0 holds
vseq # x is convergent ) & ( for x being Point of X ex K being Real st
( 0 <= K & ( for n being Nat holds ||.((vseq # x) . n).|| <= K ) ) ) holds
for x being Point of X holds vseq # x is convergent
let Y be RealBanachSpace; :: thesis: for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st X0 is dense & ( for x being Point of X st x in X0 holds
vseq # x is convergent ) & ( for x being Point of X ex K being Real st
( 0 <= K & ( for n being Nat holds ||.((vseq # x) . n).|| <= K ) ) ) holds
for x being Point of X holds vseq # x is convergent
let vseq be sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: ( X0 is dense & ( for x being Point of X st x in X0 holds
vseq # x is convergent ) & ( for x being Point of X ex K being Real st
( 0 <= K & ( for n being Nat holds ||.((vseq # x) . n).|| <= K ) ) ) implies for x being Point of X holds vseq # x is convergent )
assume A1: X0 is dense ; :: thesis: ( ex x being Point of X st
( x in X0 & not vseq # x is convergent ) or ex x being Point of X st
for K being Real holds
( not 0 <= K or ex n being Nat st not ||.((vseq # x) . n).|| <= K ) or for x being Point of X holds vseq # x is convergent )
set T = rng vseq;
assume A2: for x being Point of X st x in X0 holds
vseq # x is convergent ; :: thesis: ( ex x being Point of X st
for K being Real holds
( not 0 <= K or ex n being Nat st not ||.((vseq # x) . n).|| <= K ) or for x being Point of X holds vseq # x is convergent )
vseq in Funcs (NAT, the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))) by FUNCT_2:8;
then ex f0 being Function st
( vseq = f0 & dom f0 = NAT & rng f0 c= the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) ) by FUNCT_2:def 2;
then reconsider T = rng vseq as Subset of (R_NormSpace_of_BoundedLinearOperators (X,Y)) ;
assume A3: for x being Point of X ex K being Real st
( 0 <= K & ( for n being Nat holds ||.((vseq # x) . n).|| <= K ) ) ; :: thesis: for x being Point of X holds vseq # x is convergent
for x being Point of X ex K being Real st
( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.(f . x).|| <= K ) )
proof
let x be Point of X; :: thesis: ex K being Real st
( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.(f . x).|| <= K ) )
consider K being Real such that
A4: 0 <= K and
A5: for n being Nat holds ||.((vseq # x) . n).|| <= K by A3;
take K ; :: thesis: ( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.(f . x).|| <= K ) )
now :: thesis: for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.(f . x).|| <= K
let f be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: ( f in T implies ||.(f . x).|| <= K )
assume f in T ; :: thesis: ||.(f . x).|| <= K
then consider n being object such that
A6: n in NAT and
A7: f = vseq . n by FUNCT_2:11;
reconsider n = n as Nat by A6;
||.(f . x).|| = ||.((vseq # x) . n).|| by A7, Def2;
hence ||.(f . x).|| <= K by A5; :: thesis: verum
end;
hence ( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.(f . x).|| <= K ) ) by A4; :: thesis: verum
end;
then consider L being Real such that
A8: 0 <= L and
A9: for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= L by Th5;
set M = 1 + L;
A10: L + 0 < 1 + L by XREAL_1:8;
A11: for f being Lipschitzian LinearOperator of X,Y st f in T holds
for x, y being Point of X holds ||.((f . x) - (f . y)).|| <= (1 + L) * ||.(x - y).||
proof
let f be Lipschitzian LinearOperator of X,Y; :: thesis: ( f in T implies for x, y being Point of X holds ||.((f . x) - (f . y)).|| <= (1 + L) * ||.(x - y).|| )
reconsider f1 = f as Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) by LOPBAN_1:def 9;
assume f in T ; :: thesis: for x, y being Point of X holds ||.((f . x) - (f . y)).|| <= (1 + L) * ||.(x - y).||
then ||.f1.|| <= L by A9;
then A12: ||.f1.|| < 1 + L by A10, XXREAL_0:2;
let x, y be Point of X; :: thesis: ||.((f . x) - (f . y)).|| <= (1 + L) * ||.(x - y).||
||.((f . x) - (f . y)).|| = ||.((f . x) + ((- 1) * (f . y))).|| by RLVECT_1:16;
then ||.((f . x) - (f . y)).|| = ||.((f . x) + (f . ((- 1) * y))).|| by LOPBAN_1:def 5;
then ||.((f . x) - (f . y)).|| = ||.(f . (x + ((- 1) * y))).|| by VECTSP_1:def 20;
then A13: ||.((f . x) - (f . y)).|| = ||.(f . (x - y)).|| by RLVECT_1:16;
( ||.(f . (x - y)).|| <= ||.f1.|| * ||.(x - y).|| & ||.f1.|| * ||.(x - y).|| <= (1 + L) * ||.(x - y).|| ) by A12, LOPBAN_1:32, XREAL_1:64;
hence ||.((f . x) - (f . y)).|| <= (1 + L) * ||.(x - y).|| by A13, XXREAL_0:2; :: thesis: verum
end;
hereby :: thesis: verum
let x be Point of X; :: thesis: vseq # x is convergent
for TK1 being Real st TK1 > 0 holds
ex n0 being Nat st
for n, m being Nat st n >= n0 & m >= n0 holds
||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1
proof
let TK1 be Real; :: thesis: ( TK1 > 0 implies ex n0 being Nat st
for n, m being Nat st n >= n0 & m >= n0 holds
||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1 )
assume A14: TK1 > 0 ; :: thesis: ex n0 being Nat st
for n, m being Nat st n >= n0 & m >= n0 holds
||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1
A15: 0 < TK1 / 3 by A14, XREAL_1:222;
set V = { z where z is Point of X : ||.(x - z).|| < TK1 / (3 * (1 + L)) } ;
{ z where z is Point of X : ||.(x - z).|| < TK1 / (3 * (1 + L)) } c= the carrier of X
proof
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in { z where z is Point of X : ||.(x - z).|| < TK1 / (3 * (1 + L)) } or s in the carrier of X )
assume s in { z where z is Point of X : ||.(x - z).|| < TK1 / (3 * (1 + L)) } ; :: thesis: s in the carrier of X
then ex z being Point of X st
( s = z & ||.(x - z).|| < TK1 / (3 * (1 + L)) ) ;
hence s in the carrier of X ; :: thesis: verum
end;
then reconsider V = { z where z is Point of X : ||.(x - z).|| < TK1 / (3 * (1 + L)) } as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def 4;
reconsider TKK = TK1 as Real ;
0 < 3 * (1 + L) by A8, XREAL_1:129;
then 0 < TK1 / (3 * (1 + L)) by A14, XREAL_1:139;
then ||.(x - x).|| < TKK / (3 * (1 + L)) by NORMSP_1:6;
then ( V is open & x in V ) by NORMSP_2:23;
then X0 meets V by A1, TOPS_1:45;
then consider s being object such that
A16: s in X0 and
A17: s in V by XBOOLE_0:3;
consider y being Point of X such that
A18: s = y and
A19: ||.(x - y).|| < TK1 / (3 * (1 + L)) by A17;
for s being Real st 0 < s holds
ex n1 being Nat st
for m1 being Nat st n1 <= m1 holds
||.(((vseq # y) . m1) - ((vseq # y) . n1)).|| < s by A2, A16, A18, LOPBAN_3:4;
then vseq # y is Cauchy_sequence_by_Norm by LOPBAN_3:5;
then consider n0 being Nat such that
A20: for n, m being Nat st n >= n0 & m >= n0 holds
||.(((vseq # y) . n) - ((vseq # y) . m)).|| < TK1 / 3 by A15, RSSPACE3:8;
take n0 ; :: thesis: for n, m being Nat st n >= n0 & m >= n0 holds
||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1
for n, m being Nat st n >= n0 & m >= n0 holds
||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1
proof
let n, m be Nat; :: thesis: ( n >= n0 & m >= n0 implies ||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1 )
A21: m in NAT by ORDINAL1:def 12;
A22: n in NAT by ORDINAL1:def 12;
reconsider f = vseq . n as Lipschitzian LinearOperator of X,Y by LOPBAN_1:def 9;
reconsider g = vseq . m as Lipschitzian LinearOperator of X,Y by LOPBAN_1:def 9;
||.(((vseq # x) . n) - ((vseq # y) . m)).|| <= ||.(((vseq # x) . n) - ((vseq # y) . n)).|| + ||.(((vseq # y) . n) - ((vseq # y) . m)).|| by NORMSP_1:10;
then A23: ||.(((vseq # x) . n) - ((vseq # y) . m)).|| + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| <= (||.(((vseq # x) . n) - ((vseq # y) . n)).|| + ||.(((vseq # y) . n) - ((vseq # y) . m)).||) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| by XREAL_1:6;
assume ( n >= n0 & m >= n0 ) ; :: thesis: ||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1
then ||.(((vseq # y) . n) - ((vseq # y) . m)).|| < TK1 / 3 by A20;
then ||.(((vseq # x) . n) - ((vseq # y) . n)).|| + ||.(((vseq # y) . n) - ((vseq # y) . m)).|| < ||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3) by XREAL_1:8;
then A24: (||.(((vseq # x) . n) - ((vseq # y) . n)).|| + ||.(((vseq # y) . n) - ((vseq # y) . m)).||) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| < (||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| by XREAL_1:8;
||.(((vseq # x) . m) - ((vseq # y) . m)).|| = ||.(((vseq . m) . x) - ((vseq # y) . m)).|| by Def2;
then ||.(((vseq # x) . m) - ((vseq # y) . m)).|| = ||.((g . x) - (g . y)).|| by Def2;
then A25: ||.(((vseq # x) . m) - ((vseq # y) . m)).|| <= (1 + L) * ||.(x - y).|| by A11, FUNCT_2:4, A21;
(1 + L) * ||.(x - y).|| < (1 + L) * (TK1 / (3 * (1 + L))) by A8, A19, XREAL_1:68;
then (1 + L) * ||.(x - y).|| < TK1 / 3 by A8, XCMPLX_1:92;
then ||.(((vseq # x) . m) - ((vseq # y) . m)).|| < TK1 / 3 by A25, XXREAL_0:2;
then ||.(((vseq # y) . m) - ((vseq # x) . m)).|| < TK1 / 3 by NORMSP_1:7;
then A26: ((TK1 / 3) + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| < ((TK1 / 3) + (TK1 / 3)) + (TK1 / 3) by XREAL_1:8;
||.(((vseq # x) . n) - ((vseq # y) . n)).|| = ||.(((vseq . n) . x) - ((vseq # y) . n)).|| by Def2;
then ||.(((vseq # x) . n) - ((vseq # y) . n)).|| = ||.((f . x) - (f . y)).|| by Def2;
then A27: ||.(((vseq # x) . n) - ((vseq # y) . n)).|| <= (1 + L) * ||.(x - y).|| by A11, FUNCT_2:4, A22;
||.(((vseq # x) . n) - ((vseq # x) . m)).|| <= ||.(((vseq # x) . n) - ((vseq # y) . m)).|| + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| by NORMSP_1:10;
then ||.(((vseq # x) . n) - ((vseq # x) . m)).|| <= (||.(((vseq # x) . n) - ((vseq # y) . n)).|| + ||.(((vseq # y) . n) - ((vseq # y) . m)).||) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| by A23, XXREAL_0:2;
then A28: ||.(((vseq # x) . n) - ((vseq # x) . m)).|| < (||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| by A24, XXREAL_0:2;
(1 + L) * ||.(x - y).|| < (1 + L) * (TK1 / (3 * (1 + L))) by A8, A19, XREAL_1:68;
then (1 + L) * ||.(x - y).|| < TK1 / 3 by A8, XCMPLX_1:92;
then ||.(((vseq # x) . n) - ((vseq # y) . n)).|| < TK1 / 3 by A27, XXREAL_0:2;
then ||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3) < (TK1 / 3) + (TK1 / 3) by XREAL_1:8;
then (||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| < ((TK1 / 3) + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| by XREAL_1:8;
then (||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| < ((TK1 / 3) + (TK1 / 3)) + (TK1 / 3) by A26, XXREAL_0:2;
hence ||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1 by A28, XXREAL_0:2; :: thesis: verum
end;
hence for n, m being Nat st n >= n0 & m >= n0 holds
||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1 ; :: thesis: verum
end;
then vseq # x is Cauchy_sequence_by_Norm by RSSPACE3:8;
hence vseq # x is convergent by LOPBAN_1:def 15; :: thesis: verum
end;