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 )
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 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 )
vseq in Funcs NAT ,the carrier of (R_NormSpace_of_BoundedLinearOperators X,Y) by FUNCT_2:11;
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 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
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 ) )

proof

let x be Point of X; :: thesis: 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 ) )
consider K being real number such that
A4: 0 <= K and
A5: for n being Element of 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

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 set such that
A6: n in NAT and
A7: f = vseq . n by FUNCT_2:17;
reconsider n = n as Element of 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 number 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:10;
A11: 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).|| )
reconsider f1 = f as Point of (R_NormSpace_of_BoundedLinearOperators X,Y) by LOPBAN_1:def 10;
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: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 A13: ||.((f . x) - (f . y)).|| = ||.(f . (x - y)).|| by RLVECT_1:29;
0 <= ||.(x - y).|| by NORMSP_1:8;
then ( ||.(f . (x - y)).|| <= ||.f1.|| * ||.(x - y).|| & ||.f1.|| * ||.(x - y).|| <= (1 + L) * ||.(x - y).|| ) by A12, LOPBAN_1:38, XREAL_1:66;
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 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
A15: 0 < TK1 / 3 by A14, XREAL_1:224;
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 set ; :: 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;
0 < 3 * (1 + L) by A8, 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 ( V is open & x in V ) by NORMSP_2:23;
then X0 meets V by A1, TOPS_1:80;
then consider s being set 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 Element of NAT st
for m1 being Element of NAT st n1 <= m1 holds
||.(((vseq # y) . m1) - ((vseq # y) . n1)).|| < s by A2, A16, A18, LOPBAN_3:4;
then vseq # y is CCauchy by LOPBAN_3:5;
then consider n0 being Element of NAT such that
A20: for n, m being Element of NAT st n >= n0 & m >= n0 holds
||.(((vseq # y) . n) - ((vseq # y) . m)).|| < TK1 / 3 by A15, 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 )
reconsider f = vseq . n as bounded LinearOperator of X,Y by LOPBAN_1:def 10;
reconsider g = vseq . m as bounded LinearOperator of X,Y by LOPBAN_1:def 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;
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:10;
then A22: (||.(((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) . 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 A23: ||.(((vseq # x) . m) - ((vseq # y) . m)).|| <= (1 + L) * ||.(x - y).|| by A11, FUNCT_2:6;
(1 + L) * ||.(x - y).|| < (1 + L) * (TK1 / (3 * (1 + L))) by A8, A19, XREAL_1:70;
then (1 + L) * ||.(x - y).|| < TK1 / 3 by A8, XCMPLX_1:93;
then ||.(((vseq # x) . m) - ((vseq # y) . m)).|| < TK1 / 3 by A23, XXREAL_0:2;
then ||.(((vseq # y) . m) - ((vseq # x) . m)).|| < TK1 / 3 by NORMSP_1:11;
then A24: ((TK1 / 3) + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| < ((TK1 / 3) + (TK1 / 3)) + (TK1 / 3) by XREAL_1: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 A25: ||.(((vseq # x) . n) - ((vseq # y) . n)).|| <= (1 + L) * ||.(x - y).|| by A11, FUNCT_2:6;
||.(((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 A26: ||.(((vseq # x) . n) - ((vseq # x) . m)).|| < (||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| by A22, XXREAL_0:2;
(1 + L) * ||.(x - y).|| < (1 + L) * (TK1 / (3 * (1 + L))) by A8, A19, XREAL_1:70;
then (1 + L) * ||.(x - y).|| < TK1 / 3 by A8, XCMPLX_1:93;
then ||.(((vseq # x) . n) - ((vseq # y) . n)).|| < TK1 / 3 by A25, XXREAL_0:2;
then ||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (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)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| 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 A26, 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;