let X, Y be RealBanachSpace; for X0 being Subset of (LinearTopSpaceNorm X)
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 st
( 0 <= K & ( for n being Nat holds ||.((vseq # x) . n).|| <= K ) ) ) holds
ex tseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| )
let X0 be Subset of (LinearTopSpaceNorm X); 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 st
( 0 <= K & ( for n being Nat holds ||.((vseq # x) . n).|| <= K ) ) ) holds
ex tseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| )
let vseq be sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)); ( 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 st
( 0 <= K & ( for n being Nat holds ||.((vseq # x) . n).|| <= K ) ) ) implies ex tseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| ) )
assume A1:
X0 is dense
; ( 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 holds
( not 0 <= K or ex n being Nat st not ||.((vseq # x) . n).|| <= K ) or ex tseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| ) )
deffunc H1( Point of X) -> Element of the carrier of Y = lim (vseq # $1);
assume A2:
for x being Point of X st x in X0 holds
vseq # x is convergent
; ( ex x being Point of X st
for K being Real holds
( not 0 <= K or ex n being Nat st not ||.((vseq # x) . n).|| <= K ) or ex tseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| ) )
consider tseq being Function of X,Y such that
A3:
for x being Point of X holds tseq . x = H1(x)
from FUNCT_2:sch 4();
assume
for x being Point of X ex K being Real st
( 0 <= K & ( for n being Nat holds ||.((vseq # x) . n).|| <= K ) )
; ex tseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| )
then A4:
for x being Point of X holds vseq # x is convergent
by A1, A2, Th7;
then reconsider tseq = tseq as Lipschitzian LinearOperator of X,Y by A3, Th6;
reconsider tseq = tseq as Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) by LOPBAN_1:def 9;
take
tseq
; ( ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| )
thus
( ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| )
by A4, A3, Th6; verum