let X be RealBanachSpace; for Y being RealNormSpace
for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for tseq being Function of X,Y st ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) ) ) holds
( 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.|| ) )
let Y be RealNormSpace; for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for tseq being Function of X,Y st ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) ) ) holds
( 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.|| ) )
let vseq be sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)); for tseq being Function of X,Y st ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) ) ) holds
( 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.|| ) )
let tseq be Function of X,Y; ( ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) ) ) implies ( 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.|| ) ) )
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) )
; ( 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.|| ) )
A2:
for x, y being Point of X holds tseq . (x + y) = (tseq . x) + (tseq . y)
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 ) )
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
then A17:
||.vseq.|| is bounded
by A12, SEQ_2:3;
A18:
for x being Point of X holds ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.||
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)
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.||
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; verum