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 number st
( 0 <= K & ( for n being Element of 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 number st
( 0 <= K & ( for n being Element of 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 number st
( 0 <= K & ( for n being Element of 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 number holds
( not 0 <= K or ex n being Element of 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.|| ) )
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 number holds
( not 0 <= K or ex n being Element of 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.|| ) )
assume for x being Point of X ex K being real number st
( 0 <= K & ( for n being Element of 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 A3: for x being Point of X holds vseq # x is convergent by A1, A2, Th7;
deffunc H₁( Point of X) -> Element of the carrier of Y = lim (vseq # $1);
consider tseq being Function of X,Y such that
A4: for x being Point of X holds tseq . x = H₁(x) from FUNCT_2:sch 4();
reconsider tseq = tseq as bounded LinearOperator of X,Y by A3, A4, Th6;
reconsider tseq = tseq as Point of (R_NormSpace_of_BoundedLinearOperators X,Y) by LOPBAN_1:def 10;
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 A3, A4, Th6; :: thesis: verum