let X be RealNormSpace; :: thesis:
let L be Subset of X; :: thesis:
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:
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 ) )

let f be Point of (DualSp X); :: thesis:
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

let g be Point of (R_NormSpace_of_BoundedLinearOperators ((DualSp X),RNS_Real)); :: thesis:
assume g in (BidualFunc X) .: L ; :: thesis:
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:

end;

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

end;

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