let X be RealNormSpace; :: thesis: for L being Subset of X st not X is trivial & ( for f being Point of (DualSp X) ex Kf being Real st
( 0 <= Kf & ( for x being Point of X st x in L holds
|.(f . x).| <= Kf ) ) ) holds
ex M being Real st
( 0 <= M & ( for x being Point of X st x in L holds
||.x.|| <= M ) )
let L be Subset of X; :: thesis: ( not X is trivial & ( for f being Point of (DualSp X) ex Kf being Real st
( 0 <= Kf & ( for x being Point of X st x in L holds
|.(f . x).| <= Kf ) ) ) implies ex M being Real st
( 0 <= M & ( for x being Point of X st x in L holds
||.x.|| <= M ) ) )
assume AS: ( not X is trivial & ( for f being Point of (DualSp X) ex Kf being Real st
( 0 <= Kf & ( for x being Point of X st x in L holds
|.(f . x).| <= Kf ) ) ) ) ; :: thesis: ex M being Real st
( 0 <= M & ( for x being Point of X st x in L holds
||.x.|| <= M ) )
set T = (BidualFunc X) .: L;
XX: (BidualFunc X) .: L is Subset of (R_NormSpace_of_BoundedLinearOperators ((DualSp X),RNS_Real)) by Th75A;
for f being Point of (DualSp X) ex Kf being Real st
( 0 <= Kf & ( for g being Point of (R_NormSpace_of_BoundedLinearOperators ((DualSp X),RNS_Real)) st g in (BidualFunc X) .: L holds
||.(g . f).|| <= Kf ) )

proof

let f be Point of (DualSp X); :: thesis: ex Kf being Real st
( 0 <= Kf & ( for g being Point of (R_NormSpace_of_BoundedLinearOperators ((DualSp X),RNS_Real)) st g in (BidualFunc X) .: L holds
||.(g . f).|| <= Kf ) )
consider Kf being Real such that
A0: ( 0 <= Kf & ( for x being Point of X st x in L holds
|.(f . x).| <= Kf ) ) by AS;
for g being Point of (R_NormSpace_of_BoundedLinearOperators ((DualSp X),RNS_Real)) st g in (BidualFunc X) .: L holds
||.(g . f).|| <= Kf

proof

let g be Point of (R_NormSpace_of_BoundedLinearOperators ((DualSp X),RNS_Real)); :: thesis: ( g in (BidualFunc X) .: L implies ||.(g . f).|| <= Kf )
assume g in (BidualFunc X) .: L ; :: thesis: ||.(g . f).|| <= Kf
then consider x being object such that
A1: ( x in dom (BidualFunc X) & x in L & g = (BidualFunc X) . x ) by FUNCT_1:def 6;
reconsider x = x as Point of X by A1;
A2: |.(f . x).| <= Kf by A1, A0;
g = BiDual x by A1, Def2;
then f . x = g . f by Def1;
hence ||.(g . f).|| <= Kf by A2, EUCLID:def 2; :: thesis: verum

end;

hence ex Kf being Real st
( 0 <= Kf & ( for g being Point of (R_NormSpace_of_BoundedLinearOperators ((DualSp X),RNS_Real)) st g in (BidualFunc X) .: L holds
||.(g . f).|| <= Kf ) ) by A0; :: thesis: verum

end;

then consider M being Real such that
B0: ( 0 <= M & ( for g being Point of (R_NormSpace_of_BoundedLinearOperators ((DualSp X),RNS_Real)) st g in (BidualFunc X) .: L holds
||.g.|| <= M ) ) by XX, LOPBAN_5:5;
B1: for x being Point of X st x in L holds
||.x.|| <= M

proof

let x be Point of X; :: thesis: ( x in L implies ||.x.|| <= M )
assume B2: x in L ; :: thesis: ||.x.|| <= M
x in the carrier of X ;
then B3: x in dom (BidualFunc X) by FUNCT_2:def 1;
reconsider g = (BidualFunc X) . x as Point of (R_NormSpace_of_BoundedLinearOperators ((DualSp X),RNS_Real)) by Th75A;
B4: g in (BidualFunc X) .: L by B2, B3, FUNCT_1:def 6;
||.x.|| = ||.((BidualFunc X) . x).|| by AS, LMNORM
.= ||.g.|| by LMN11 ;
hence ||.x.|| <= M by B0, B4; :: thesis: verum

end;

take M ; :: thesis: ( 0 <= M & ( for x being Point of X st x in L holds
||.x.|| <= M ) )
thus ( 0 <= M & ( for x being Point of X st x in L holds
||.x.|| <= M ) ) by B1, B0; :: thesis: verum