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 number st
( 0 <= K & ( for n being Element of 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 number st
( 0 <= K & ( for n being Element of 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 number st
( 0 <= K & ( for n being Element of 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 number st
( 0 <= K & ( for n being Element of 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 number holds
( not 0 <= K or ex n being Element of NAT st not ||.((vseq # x) . n).|| <= K ) or for x being Point of X holds vseq # x is convergent )
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 number holds
( not 0 <= K or ex n being Element of NAT st not ||.((vseq # x) . n).|| <= K ) or for x being Point of X holds vseq # x is convergent )
assume A3:
for x being Point of X ex K being real number st
( 0 <= K & ( for n being Element of NAT holds ||.((vseq # x) . n).|| <= K ) )
; :: thesis: for x being Point of X holds vseq # x is convergent
set T = rng vseq;
vseq in Funcs NAT ,the carrier of (R_NormSpace_of_BoundedLinearOperators X,Y)
by FUNCT_2:11;
then consider f0 being Function such that
A4:
( vseq = f0 & dom f0 = NAT & rng f0 c= the carrier of (R_NormSpace_of_BoundedLinearOperators X,Y) )
by FUNCT_2:def 2;
reconsider T = rng vseq as Subset of (R_NormSpace_of_BoundedLinearOperators X,Y) by A4;
for x being Point of X ex K being real number st
( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators X,Y) st f in T holds
||.(f . x).|| <= K ) )
then consider L being real number such that
A7:
( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators X,Y) st f in T holds
||.f.|| <= L ) )
by Th5;
set M = 1 + L;
A8:
L + 0 < 1 + L
by XREAL_1:10;
A9:
for f being bounded 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
bounded 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).|| )
assume A10:
f in T
;
:: thesis: for x, y being Point of X holds ||.((f . x) - (f . y)).|| <= (1 + L) * ||.(x - y).||
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:29;
then
||.((f . x) - (f . y)).|| = ||.((f . x) + (f . ((- 1) * y))).||
by LOPBAN_1:def 6;
then
||.((f . x) - (f . y)).|| = ||.(f . (x + ((- 1) * y))).||
by LOPBAN_1:def 5;
then A11:
||.((f . x) - (f . y)).|| = ||.(f . (x - y)).||
by RLVECT_1:29;
reconsider f1 =
f as
Point of
(R_NormSpace_of_BoundedLinearOperators X,Y) by LOPBAN_1:def 10;
A12:
||.(f . (x - y)).|| <= ||.f1.|| * ||.(x - y).||
by LOPBAN_1:38;
||.f1.|| <= L
by A7, A10;
then A13:
||.f1.|| < 1
+ L
by A8, XXREAL_0:2;
0 <= ||.(x - y).||
by NORMSP_1:8;
then
||.f1.|| * ||.(x - y).|| <= (1 + L) * ||.(x - y).||
by A13, XREAL_1:66;
hence
||.((f . x) - (f . y)).|| <= (1 + L) * ||.(x - y).||
by A11, A12, 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
Element of
NAT st
for
n,
m being
Element of
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 Element of NAT st
for n, m being Element of NAT st n >= n0 & m >= n0 holds
||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1 )
assume A14:
TK1 > 0
;
:: thesis: ex n0 being Element of NAT st
for n, m being Element of NAT st n >= n0 & m >= n0 holds
||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1
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
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;
A15:
V is
open
by NORMSP_2:23;
0 < 3
* (1 + L)
by A7, XREAL_1:131;
then
0 < TK1 / (3 * (1 + L))
by A14, XREAL_1:141;
then
||.(x - x).|| < TK1 / (3 * (1 + L))
by NORMSP_1:10;
then
x in V
;
then
X0 meets V
by A1, A15, TOPS_1:80;
then consider s being
set such that A16:
(
s in X0 &
s in V )
by XBOOLE_0:3;
consider y being
Point of
X such that A17:
(
s = y &
||.(x - y).|| < TK1 / (3 * (1 + L)) )
by A16;
for
s being
Real st
0 < s holds
ex
n1 being
Element of
NAT st
for
m1 being
Element of
NAT st
n1 <= m1 holds
||.(((vseq # y) . m1) - ((vseq # y) . n1)).|| < s
by A2, A16, A17, LOPBAN_3:4;
then A18:
vseq # y is
CCauchy
by LOPBAN_3:5;
0 < TK1 / 3
by A14, XREAL_1:224;
then consider n0 being
Element of
NAT such that A19:
for
n,
m being
Element of
NAT st
n >= n0 &
m >= n0 holds
||.(((vseq # y) . n) - ((vseq # y) . m)).|| < TK1 / 3
by A18, RSSPACE3:10;
take
n0
;
:: thesis: for n, m being Element of NAT st n >= n0 & m >= n0 holds
||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1
for
n,
m being
Element of
NAT st
n >= n0 &
m >= n0 holds
||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1
proof
let n,
m be
Element of
NAT ;
:: thesis: ( n >= n0 & m >= n0 implies ||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1 )
assume
(
n >= n0 &
m >= n0 )
;
:: thesis: ||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1
then
||.(((vseq # y) . n) - ((vseq # y) . m)).|| < TK1 / 3
by A19;
then
||.(((vseq # x) . n) - ((vseq # y) . n)).|| + ||.(((vseq # y) . n) - ((vseq # y) . m)).|| < ||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3)
by XREAL_1:10;
then A20:
(||.(((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:10;
||.(((vseq # x) . n) - ((vseq # y) . m)).|| <= ||.(((vseq # x) . n) - ((vseq # y) . n)).|| + ||.(((vseq # y) . n) - ((vseq # y) . m)).||
by NORMSP_1:14;
then A21:
||.(((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:8;
||.(((vseq # x) . n) - ((vseq # x) . m)).|| <= ||.(((vseq # x) . n) - ((vseq # y) . m)).|| + ||.(((vseq # y) . m) - ((vseq # x) . m)).||
by NORMSP_1:14;
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 A21, XXREAL_0:2;
then A22:
||.(((vseq # x) . n) - ((vseq # x) . m)).|| < (||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).||
by A20, XXREAL_0:2;
reconsider f =
vseq . n as
bounded LinearOperator of
X,
Y by LOPBAN_1:def 10;
||.(((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 A23:
||.(((vseq # x) . n) - ((vseq # y) . n)).|| <= (1 + L) * ||.(x - y).||
by A9, FUNCT_2:6;
(1 + L) * ||.(x - y).|| < (1 + L) * (TK1 / (3 * (1 + L)))
by A7, A17, XREAL_1:70;
then
(1 + L) * ||.(x - y).|| < TK1 / 3
by A7, XCMPLX_1:93;
then
||.(((vseq # x) . n) - ((vseq # y) . n)).|| < TK1 / 3
by A23, XXREAL_0:2;
then
||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3) < (TK1 / 3) + (TK1 / 3)
by XREAL_1:10;
then A24:
(||.(((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:10;
reconsider g =
vseq . m as
bounded LinearOperator of
X,
Y by LOPBAN_1:def 10;
||.(((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 A9, FUNCT_2:6;
(1 + L) * ||.(x - y).|| < (1 + L) * (TK1 / (3 * (1 + L)))
by A7, A17, XREAL_1:70;
then
(1 + L) * ||.(x - y).|| < TK1 / 3
by A7, XCMPLX_1:93;
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:11;
then
((TK1 / 3) + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| < ((TK1 / 3) + (TK1 / 3)) + (TK1 / 3)
by XREAL_1:10;
then
(||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| < ((TK1 / 3) + (TK1 / 3)) + (TK1 / 3)
by A24, XXREAL_0:2;
hence
||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1
by A22, XXREAL_0:2;
:: thesis: verum
end;
hence
for
n,
m being
Element of
NAT st
n >= n0 &
m >= n0 holds
||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1
;
:: thesis: verum
end; then
vseq # x is
CCauchy
by RSSPACE3:10;
hence
vseq # x is
convergent
by LOPBAN_1:def 16;
:: thesis: verum
end;