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:
set T = rng vseq;
set RNS = R_NormSpace_of_BoundedLinearOperators X,Y;
assume A1: for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) ) ; :: thesis:
A2: for x, y being Point of X holds tseq . (x + y) = (tseq . x) + (tseq . y)

proof

let x, y be Point of X; :: thesis:
A3: ( vseq # y is convergent & tseq . y = lim (vseq # y) ) by A1;
A4: tseq . (x + y) = lim (vseq # (x + y)) by A1;

now

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

end;

then A6: vseq # (x + y) = (vseq # x) + (vseq # y) by NORMSP_1:def 5;
( vseq # x is convergent & tseq . x = lim (vseq # x) ) by A1;
hence tseq . (x + y) = (tseq . x) + (tseq . y) by A3, A6, A4, NORMSP_1:42; :: thesis:

end;

A7: 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
A8: for n being Element of NAT holds ||.(vseq # x).|| . n < K by SEQ_2:def 3;
A9: 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
A10: n in NAT and
A11: f = vseq . n by FUNCT_2:17;
reconsider n = n as Element of NAT by A10;
(vseq . n) . x = (vseq # x) . n by Def2;
then ||.(f . x).|| = ||.(vseq # x).|| . n by A11, NORMSP_1:def 10;
hence ||.(f . x).|| <= K by A8; :: thesis:

end;

||.(vseq # x).|| . 0 < K by A8;
then ||.((vseq # x) . 0 ).|| < K by NORMSP_1:def 10;
then 0 <= K by NORMSP_1:8;
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 A9; :: thesis:

end;

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 consider L being real number such that
A12: 0 <= L and
A13: for f being Point of (R_NormSpace_of_BoundedLinearOperators X,Y) st f in rng vseq holds
||.f.|| <= L by A7, Th5;
A14: 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 A13, FUNCT_2:6;
then ||.vseq.|| . n <= L by NORMSP_1:def 10;
then A15: ||.vseq.|| . n < 1 + L by A14, 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 A15, ABSVALUE:def 1; :: thesis:

end;

then A16: ||.vseq.|| is bounded by A12, SEQ_2:15;
A17: for x being Point of X holds ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.||

proof

let x be Point of X; :: thesis:
A18: ||.x.|| (#) ||.vseq.|| is bounded by A16, SEQM_3:70;
A19: for n being Element of NAT holds ||.((vseq # x) . n).|| <= ||.(vseq . n).|| * ||.x.||

proof

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

end;

A20: for n being Element of NAT holds ||.(vseq # x).|| . n <= (||.x.|| (#) ||.vseq.||) . n

proof

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

end;

A22: lim_inf (||.x.|| (#) ||.vseq.||) = (lim_inf ||.vseq.||) * ||.x.|| by A16, Th1, NORMSP_1:8;
A23: ( vseq # x is convergent & tseq . x = lim (vseq # x) ) by A1;
then ||.(vseq # x).|| is convergent by LOPBAN_1:24;
then A24: lim ||.(vseq # x).|| = lim_inf ||.(vseq # x).|| by RINFSUP1:91;
||.(vseq # x).|| is bounded by A23, LOPBAN_1:24, SEQ_2:27;
then lim_inf ||.(vseq # x).|| <= lim_inf (||.x.|| (#) ||.vseq.||) by A18, A20, RINFSUP1:93;
hence ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| by A23, A22, A24, LOPBAN_1:24; :: thesis:

end;

now

let s be real number ; :: thesis:
assume A25: 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 A25; :: 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 A26: 0 <= lim_inf ||.vseq.|| by A16, RINFSUP1:84;
A27: 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:
A28: tseq . x = lim (vseq # x) by A1;

A29: now

let n be Element of NAT ; :: thesis:
( vseq . n is bounded LinearOperator of X,Y & (vseq # (r * x)) . n = (vseq . n) . (r * x) ) by Def2, LOPBAN_1:def 10;
then (vseq # (r * x)) . n = r * ((vseq . n) . x) by 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 A29, NORMSP_1:def 8;
hence tseq . (r * x) = r * (tseq . x) by A1, A28, NORMSP_1:45; :: thesis:

end;

then reconsider tseq1 = tseq as bounded LinearOperator of X,Y by A2, A17, A26, 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

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
A30: ( k = ||.(tseq . x).|| & ||.x.|| <= 1 ) ;
( k <= (lim_inf ||.vseq.||) * ||.x.|| & (lim_inf ||.vseq.||) * ||.x.|| <= lim_inf ||.vseq.|| ) by A17, A26, A30, XREAL_1:155;
hence k <= lim_inf ||.vseq.|| by XXREAL_0:2; :: thesis:

end;

then A31: sup (PreNorms tseq1) <= lim_inf ||.vseq.|| by SEQ_4:62;
let ttseq be Point of (R_NormSpace_of_BoundedLinearOperators X,Y); :: thesis:
assume ttseq = tseq ; :: thesis:
hence ||.ttseq.|| <= lim_inf ||.vseq.|| by A31, 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 A2, A27, A17, A26, LOPBAN_1:def 5, LOPBAN_1:def 6, LOPBAN_1:def 9; :: thesis: