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 :: thesis:

let n be Nat; :: thesis:
( vseq . n is Lipschitzian LinearOperator of X,Y & (vseq # (x + y)) . n = (vseq . n) . (x + y) ) by Def2, LOPBAN_1:def 9;
then A5: (vseq # (x + y)) . n = ((vseq . n) . x) + ((vseq . n) . y) by VECTSP_1:def 20;
(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 2;
( 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:25; :: thesis:

end;

A7: 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 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:23, SEQ_2:13;
then consider K being Real such that
A8: for n being 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 object such that
A10: n in NAT and
A11: f = vseq . n by FUNCT_2:11;
reconsider n = n as Nat by A10;
(vseq . n) . x = (vseq # x) . n by Def2;
then ||.(f . x).|| = ||.(vseq # x).|| . n by A11, NORMSP_0:def 4;
hence ||.(f . x).|| <= K by A8; :: thesis:

end;

||.(vseq # x).|| . 0 < K by A8;
then ||.((vseq # x) . 0).|| < K by NORMSP_0:def 4;
then 0 <= K ;
hence ex K being Real 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: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 consider L being Real 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:8;
for n being Nat holds |.(||.vseq.|| . n).| < 1 + L

proof

let n be Nat; :: thesis:
A15: n in NAT by ORDINAL1:def 12;
||.(vseq . n).|| <= L by A13, FUNCT_2:4, A15;
then ||.vseq.|| . n <= L by NORMSP_0:def 4;
then A16: ||.vseq.|| . n < 1 + L by A14, XXREAL_0:2;
0 <= ||.(vseq . n).|| ;
then 0 <= ||.vseq.|| . n by NORMSP_0:def 4;
hence |.(||.vseq.|| . n).| < 1 + L by A16, ABSVALUE:def 1; :: thesis:

end;

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

proof

let x be Point of X; :: thesis:
A19: ||.x.|| (#) ||.vseq.|| is bounded by A17, SEQM_3:37;
A20: for n being Nat holds ||.((vseq # x) . n).|| <= ||.(vseq . n).|| * ||.x.||

proof

let n be Nat; :: thesis:
( (vseq . n) . x = (vseq # x) . n & vseq . n is Lipschitzian LinearOperator of X,Y ) by Def2, LOPBAN_1:def 9;
hence ||.((vseq # x) . n).|| <= ||.(vseq . n).|| * ||.x.|| by LOPBAN_1:32; :: thesis:

end;

A21: for n being Nat holds ||.(vseq # x).|| . n <= (||.x.|| (#) ||.vseq.||) . n

proof

let n be Nat; :: thesis:
A22: ||.(vseq . n).|| = ||.vseq.|| . n by NORMSP_0:def 4;
( ||.(vseq # x).|| . n = ||.((vseq # x) . n).|| & ||.((vseq # x) . n).|| <= ||.(vseq . n).|| * ||.x.|| ) by A20, NORMSP_0:def 4;
hence ||.(vseq # x).|| . n <= (||.x.|| (#) ||.vseq.||) . n by A22, SEQ_1:9; :: thesis:

end;

A23: lim_inf (||.x.|| (#) ||.vseq.||) = (lim_inf ||.vseq.||) * ||.x.|| by A17, Th1;
A24: ( vseq # x is convergent & tseq . x = lim (vseq # x) ) by A1;
then ||.(vseq # x).|| is convergent by LOPBAN_1:20;
then A25: lim ||.(vseq # x).|| = lim_inf ||.(vseq # x).|| by RINFSUP1:89;
||.(vseq # x).|| is bounded by A24, LOPBAN_1:20, SEQ_2:13;
then lim_inf ||.(vseq # x).|| <= lim_inf (||.x.|| (#) ||.vseq.||) by A19, A21, RINFSUP1:91;
hence ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| by A24, A23, A25, LOPBAN_1:20; :: thesis:

end;

now :: thesis:

let s be Real; :: thesis:
assume A26: 0 < s ; :: thesis:
for k being Nat holds 0 - s < ||.vseq.|| . (0 + k)

proof

let k be Nat; :: thesis:
||.(vseq . k).|| = ||.vseq.|| . k by NORMSP_0:def 4;
then 0 <= ||.vseq.|| . k ;
hence 0 - s < ||.vseq.|| . (0 + k) by A26; :: thesis:

end;

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

end;

then A27: 0 <= lim_inf ||.vseq.|| by A17, RINFSUP1:82;
A28: for x being Point of X
for r being Real holds tseq . (r * x) = r * (tseq . x)

proof

let x be Point of X; :: thesis:
let r be Real; :: thesis:
A29: tseq . x = lim (vseq # x) by A1;

A30: now :: thesis:

let n be Nat; :: thesis:
( vseq . n is Lipschitzian LinearOperator of X,Y & (vseq # (r * x)) . n = (vseq . n) . (r * x) ) by Def2, LOPBAN_1:def 9;
then (vseq # (r * x)) . n = r * ((vseq . n) . x) by LOPBAN_1:def 5;
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 A30, NORMSP_1:def 5;
hence tseq . (r * x) = r * (tseq . x) by A1, A29, NORMSP_1:28; :: thesis:

end;

then reconsider tseq1 = tseq as Lipschitzian LinearOperator of X,Y by A2, A18, A27, LOPBAN_1:def 5, LOPBAN_1:def 8, VECTSP_1:def 20;
for ttseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ttseq = tseq holds
||.ttseq.|| <= lim_inf ||.vseq.||

proof

for k being Real st k in { ||.(tseq . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } holds
k <= lim_inf ||.vseq.||

proof

let k be Real; :: thesis:
assume k in { ||.(tseq . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } ; :: thesis:
then consider x being Point of X such that
A31: ( k = ||.(tseq . x).|| & ||.x.|| <= 1 ) ;
( k <= (lim_inf ||.vseq.||) * ||.x.|| & (lim_inf ||.vseq.||) * ||.x.|| <= lim_inf ||.vseq.|| ) by A18, A27, A31, XREAL_1:153;
hence k <= lim_inf ||.vseq.|| by XXREAL_0:2; :: thesis:

end;

then A32: upper_bound (PreNorms tseq1) <= lim_inf ||.vseq.|| by SEQ_4:45;
let ttseq be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis:
assume ttseq = tseq ; :: thesis:
hence ||.ttseq.|| <= lim_inf ||.vseq.|| by A32, LOPBAN_1:30; :: thesis:

end;

hence ( tseq is Lipschitzian 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, A28, A18, A27, LOPBAN_1:def 5, LOPBAN_1:def 8, VECTSP_1:def 20; :: thesis: