let X, Y be RealBanachSpace; :: thesis: 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); :: thesis: 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)); :: thesis: ( 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 ; :: thesis: ( 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 H₁( 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 ; :: thesis: ( 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 = H₁(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 ) ) ; :: thesis: 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 ; :: thesis: ( ( 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; :: thesis: verum