let X be RealBanachSpace; :: thesis:
let Y be RealNormSpace; :: thesis:
let vseq be sequence of (R_NormSpace_of_BoundedLinearOperators X,Y); :: thesis:
let tseq be Function of X,Y; :: thesis:
assume A1: for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) ) ; :: thesis:
set T = rng vseq;
set RNS = R_NormSpace_of_BoundedLinearOperators X,Y;
vseq in Funcs NAT ,the carrier of (R_NormSpace_of_BoundedLinearOperators X,Y) by FUNCT_2:11;
then consider f0 being Function such that
A2: ( vseq = f0 & dom f0 = NAT & rng f0 c= the carrier of (R_NormSpace_of_BoundedLinearOperators X,Y) ) by FUNCT_2:def 2;
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 rng vseq holds
||.(f . x).|| <= K ) )

proof

let x be Point of X; :: thesis:
vseq # x is convergent by A1;
then ||.(vseq # x).|| is bounded by NORMSP_1:39, SEQ_2:27;
then consider K being real number such that
A3: for n being Element of NAT holds ||.(vseq # x).|| . n < K by SEQ_2:def 3;
||.(vseq # x).|| . 0 < K by A3;
then ||.((vseq # x) . 0 ).|| < K by NORMSP_1:def 10;
then A4: 0 <= K by NORMSP_1:8;
for f being Point of (R_NormSpace_of_BoundedLinearOperators X,Y) st f in rng vseq holds
||.(f . x).|| <= K

proof

let f be Point of (R_NormSpace_of_BoundedLinearOperators X,Y); :: thesis:
assume f in rng vseq ; :: thesis:
then consider n being set such that
A5: ( n in NAT & f = vseq . n ) by FUNCT_2:17;
reconsider n = n as Element of NAT by A5;
(vseq . n) . x = (vseq # x) . n by Def2;
then ||.(f . x).|| = ||.(vseq # x).|| . n by A5, NORMSP_1:def 10;
hence ||.(f . x).|| <= K by A3; :: thesis:

end;

hence ex K being real number st
( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators X,Y) st f in rng vseq holds
||.(f . x).|| <= K ) ) by A4; :: thesis:

end;

then consider L being real number such that
A6: ( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators X,Y) st f in rng vseq holds
||.f.|| <= L ) ) by A2, Th5;
A7: L + 0 < 1 + L by XREAL_1:10;
for n being Element of NAT holds abs (||.vseq.|| . n) < 1 + L

proof

let n be Element of NAT ; :: thesis:
||.(vseq . n).|| <= L by A6, FUNCT_2:6;
then ||.vseq.|| . n <= L by NORMSP_1:def 10;
then A8: ||.vseq.|| . n < 1 + L by A7, XXREAL_0:2;
0 <= ||.(vseq . n).|| by NORMSP_1:8;
then 0 <= ||.vseq.|| . n by NORMSP_1:def 10;
hence abs (||.vseq.|| . n) < 1 + L by A8, ABSVALUE:def 1; :: thesis:

end;

then A9: ||.vseq.|| is bounded by A6, SEQ_2:15;
A10: for x, y being Point of X holds tseq . (x + y) = (tseq . x) + (tseq . y)

proof

let x, y be Point of X; :: thesis:
A11: ( ( for n being Element of NAT holds (vseq . n) . x = (vseq # x) . n ) & vseq # x is convergent & tseq . x = lim (vseq # x) ) by A1, Def2;
A12: ( ( for n being Element of NAT holds (vseq . n) . y = (vseq # y) . n ) & vseq # y is convergent & tseq . y = lim (vseq # y) ) by A1, Def2;

now

let n be Element of NAT ; :: thesis:
A13: (vseq . n) . y = (vseq # y) . n by Def2;
A14: vseq . n is bounded LinearOperator of X,Y by LOPBAN_1:def 10;
(vseq # (x + y)) . n = (vseq . n) . (x + y) by Def2;
then (vseq # (x + y)) . n = ((vseq . n) . x) + ((vseq . n) . y) by A14, LOPBAN_1:def 5;
hence (vseq # (x + y)) . n = ((vseq # x) . n) + ((vseq # y) . n) by A13, Def2; :: thesis:

end;

then A15: vseq # (x + y) = (vseq # x) + (vseq # y) by NORMSP_1:def 5;
tseq . (x + y) = lim (vseq # (x + y)) by A1;
hence tseq . (x + y) = (tseq . x) + (tseq . y) by A11, A12, A15, NORMSP_1:42; :: thesis:

end;

A16: for x being Point of X
for r being Element of REAL holds tseq . (r * x) = r * (tseq . x)

proof

let x be Point of X; :: thesis:
let r be Element of REAL ; :: thesis:
A17: ( ( for n being Element of NAT holds (vseq . n) . x = (vseq # x) . n ) & vseq # x is convergent & tseq . x = lim (vseq # x) ) by A1, Def2;

A18: now

let n be Element of NAT ; :: thesis:
A19: vseq . n is bounded LinearOperator of X,Y by LOPBAN_1:def 10;
(vseq # (r * x)) . n = (vseq . n) . (r * x) by Def2;
then (vseq # (r * x)) . n = r * ((vseq . n) . x) by A19, LOPBAN_1:def 6;
hence (vseq # (r * x)) . n = r * ((vseq # x) . n) by Def2; :: thesis:

end;

tseq . (r * x) = lim (vseq # (r * x)) by A1;
then tseq . (r * x) = lim (r * (vseq # x)) by A18, NORMSP_1:def 8;
hence tseq . (r * x) = r * (tseq . x) by A17, NORMSP_1:45; :: thesis:

end;

A20: for x being Point of X holds ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.||

proof

let x be Point of X; :: thesis:
A21: for n being Element of NAT holds ||.((vseq # x) . n).|| <= ||.(vseq . n).|| * ||.x.||

proof

let n be Element of NAT ; :: thesis:
A22: (vseq . n) . x = (vseq # x) . n by Def2;
vseq . n is bounded LinearOperator of X,Y by LOPBAN_1:def 10;
hence ||.((vseq # x) . n).|| <= ||.(vseq . n).|| * ||.x.|| by A22, LOPBAN_1:38; :: thesis:

end;

A23: ( ( for n being Element of NAT holds (vseq . n) . x = (vseq # x) . n ) & vseq # x is convergent & tseq . x = lim (vseq # x) ) by A1, Def2;
then A24: ||.(vseq # x).|| is convergent by LOPBAN_1:24;
then A25: ||.(vseq # x).|| is bounded by SEQ_2:27;
A26: ||.x.|| (#) ||.vseq.|| is bounded by A9, SEQM_3:70;
A27: for n being Element of NAT holds ||.(vseq # x).|| . n <= (||.x.|| (#) ||.vseq.||) . n

proof

let n be Element of NAT ; :: thesis:
A28: ||.(vseq # x).|| . n = ||.((vseq # x) . n).|| by NORMSP_1:def 10;
A29: ||.((vseq # x) . n).|| <= ||.(vseq . n).|| * ||.x.|| by A21;
||.(vseq . n).|| = ||.vseq.|| . n by NORMSP_1:def 10;
hence ||.(vseq # x).|| . n <= (||.x.|| (#) ||.vseq.||) . n by A28, A29, SEQ_1:13; :: thesis:

end;

A30: lim_inf (||.x.|| (#) ||.vseq.||) = (lim_inf ||.vseq.||) * ||.x.|| by A9, Th1, NORMSP_1:8;
A31: lim ||.(vseq # x).|| = lim_inf ||.(vseq # x).|| by A24, RINFSUP1:91;
lim_inf ||.(vseq # x).|| <= lim_inf (||.x.|| (#) ||.vseq.||) by A25, A26, A27, RINFSUP1:93;
hence ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| by A23, A30, A31, LOPBAN_1:24; :: thesis:

end;

now

let s be real number ; :: thesis:
assume A32: 0 < s ; :: thesis:
for k being Element of NAT holds 0 - s < ||.vseq.|| . (0 + k)

proof

let k be Element of NAT ; :: thesis:
||.(vseq . k).|| = ||.vseq.|| . k by NORMSP_1:def 10;
then 0 <= ||.vseq.|| . k by NORMSP_1:8;
hence 0 - s < ||.vseq.|| . (0 + k) by A32; :: thesis:

end;

hence ex n being Element of NAT st
for k being Element of NAT holds 0 - s < ||.vseq.|| . (n + k) ; :: thesis:

end;

then A33: 0 <= lim_inf ||.vseq.|| by A9, RINFSUP1:84;
then reconsider tseq1 = tseq as bounded LinearOperator of X,Y by A10, A16, A20, LOPBAN_1:def 5, LOPBAN_1:def 6, LOPBAN_1:def 9;
for ttseq being Point of (R_NormSpace_of_BoundedLinearOperators X,Y) st ttseq = tseq holds
||.ttseq.|| <= lim_inf ||.vseq.||

proof

let ttseq be Point of (R_NormSpace_of_BoundedLinearOperators X,Y); :: thesis:
assume A34: ttseq = tseq ; :: thesis:
for k being real number st k in { ||.(tseq . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } holds
k <= lim_inf ||.vseq.||

proof

let k be real number ; :: thesis:
assume k in { ||.(tseq . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } ; :: thesis:
then consider x being Point of X such that
A35: ( k = ||.(tseq . x).|| & ||.x.|| <= 1 ) ;
A36: k <= (lim_inf ||.vseq.||) * ||.x.|| by A20, A35;
(lim_inf ||.vseq.||) * ||.x.|| <= lim_inf ||.vseq.|| by A33, A35, XREAL_1:155;
hence k <= lim_inf ||.vseq.|| by A36, XXREAL_0:2; :: thesis:

end;

then sup (PreNorms tseq1) <= lim_inf ||.vseq.|| by SEQ_4:62;
hence ||.ttseq.|| <= lim_inf ||.vseq.|| by A34, LOPBAN_1:36; :: thesis:

end;

hence ( tseq is bounded LinearOperator of X,Y & ( for x being Point of X holds ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) & ( for ttseq being Point of (R_NormSpace_of_BoundedLinearOperators X,Y) st ttseq = tseq holds
||.ttseq.|| <= lim_inf ||.vseq.|| ) ) by A10, A16, A20, A33, LOPBAN_1:def 5, LOPBAN_1:def 6, LOPBAN_1:def 9; :: thesis: