let X be RealNormSpace; :: thesis: for L being non empty Subset of X st not X is trivial & ( for f being Point of (DualSp X) ex Y1 being Subset of REAL st
( Y1 = { |.(f . x).| where x is Point of X : x in L } & sup Y1 < +infty ) ) holds
ex Y being Subset of REAL st
( Y = { ||.x.|| where x is Point of X : x in L } & sup Y < +infty )
let L be non empty Subset of X; :: thesis: ( not X is trivial & ( for f being Point of (DualSp X) ex Y1 being Subset of REAL st
( Y1 = { |.(f . x).| where x is Point of X : x in L } & sup Y1 < +infty ) ) implies ex Y being Subset of REAL st
( Y = { ||.x.|| where x is Point of X : x in L } & sup Y < +infty ) )
assume that
A1: not X is trivial and
A2: for f being Point of (DualSp X) ex Y1 being Subset of REAL st
( Y1 = { |.(f . x).| where x is Point of X : x in L } & sup Y1 < +infty ) ; :: thesis: ex Y being Subset of REAL st
( Y = { ||.x.|| where x is Point of X : x in L } & sup Y < +infty )
A3: 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 ) )

proof

let f be Point of (DualSp X); :: thesis: ex Kf being Real st
( 0 <= Kf & ( for x being Point of X st x in L holds
|.(f . x).| <= Kf ) )
reconsider f1 = f as Lipschitzian linear-Functional of X by DUALSP01:def 10;
consider Y1 being Subset of REAL such that
B1: ( Y1 = { |.(f . x).| where x is Point of X : x in L } & sup Y1 < +infty ) by A2;
reconsider r0 = 0 as Real ;
for r being ExtReal st r in Y1 holds
r0 <= r

proof

let r be ExtReal; :: thesis: ( r in Y1 implies r0 <= r )
assume r in Y1 ; :: thesis: r0 <= r
then ex x being Point of X st
( r = |.(f . x).| & x in L ) by B1;
hence r0 <= r by COMPLEX1:46; :: thesis: verum

end;

then U5: r0 is LowerBound of Y1 by XXREAL_2:def 2;
then U3: r0 <= inf Y1 by XXREAL_2:def 4;
consider x0 being object such that
B11: x0 in L by XBOOLE_0:def 1;
reconsider x0 = x0 as Point of X by B11;
set y1 = |.(f . x0).|;
|.(f . x0).| in Y1 by B1, B11;
then U6: ( inf Y1 <= |.(f . x0).| & |.(f . x0).| <= sup Y1 ) by XXREAL_2:3, XXREAL_2:4;
then B2: sup Y1 in REAL by B1, U3, XXREAL_0:14;
reconsider Kf = sup Y1 as Real by B2;
BX: for x being Point of X st x in L holds
|.(f . x).| <= Kf

proof

let x be Point of X; :: thesis: ( x in L implies |.(f . x).| <= Kf )
assume C0: x in L ; :: thesis: |.(f . x).| <= Kf
reconsider r = |.(f . x).| as Real ;
r in Y1 by C0, B1;
hence |.(f . x).| <= Kf by XXREAL_2:4; :: thesis: verum

end;

take Kf ; :: thesis: ( 0 <= Kf & ( for x being Point of X st x in L holds
|.(f . x).| <= Kf ) )
thus ( 0 <= Kf & ( for x being Point of X st x in L holds
|.(f . x).| <= Kf ) ) by U5, U6, BX, XXREAL_2:def 4; :: thesis: verum

end;

consider M being Real such that
D1: ( 0 <= M & ( for x being Point of X st x in L holds
||.x.|| <= M ) ) by A1, A3, Th75;
set f = 0. (DualSp X);
consider x0 being object such that
B11: x0 in L by XBOOLE_0:def 1;
reconsider x0 = x0 as Point of X by B11;
set y1 = |.((0. (DualSp X)) . x0).|;
set Y = { ||.x.|| where x is Point of X : x in L } ;
D2: ||.x0.|| in { ||.x.|| where x is Point of X : x in L } by B11;
{ ||.x.|| where x is Point of X : x in L } c= REAL

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { ||.x.|| where x is Point of X : x in L } or z in REAL )
assume z in { ||.x.|| where x is Point of X : x in L } ; :: thesis: z in REAL
then ex x being Point of X st
( z = ||.x.|| & x in L ) ;
hence z in REAL ; :: thesis: verum

end;

then reconsider Y = { ||.x.|| where x is Point of X : x in L } as non empty Subset of REAL by D2;
for r being ExtReal st r in Y holds
r <= M

proof

let r be ExtReal; :: thesis: ( r in Y implies r <= M )
assume r in Y ; :: thesis: r <= M
then ex x being Point of X st
( r = ||.x.|| & x in L ) ;
hence r <= M by D1; :: thesis: verum

end;

then M is UpperBound of Y by XXREAL_2:def 1;
then D3: sup Y <= M by XXREAL_2:def 3;
take Y ; :: thesis: ( Y = { ||.x.|| where x is Point of X : x in L } & sup Y < +infty )
M in REAL by XREAL_0:def 1;
hence ( Y = { ||.x.|| where x is Point of X : x in L } & sup Y < +infty ) by D3, XXREAL_0:2, XXREAL_0:9; :: thesis: verum