let V be RealNormSpace; :: thesis: for X being SubRealNormSpace of V
for f being Lipschitzian linear-Functional of X
for F being Point of (DualSp X) st f = F & ( for x being VECTOR of X
for v being VECTOR of V st x = v holds
f . x <= ||.v.|| ) holds
ex g being Lipschitzian linear-Functional of V ex G being Point of (DualSp V) st
( g = G & g | the carrier of X = f & ( for x being VECTOR of V holds
( g . x <= ||.x.|| & ||.G.|| = ||.F.|| ) ) )
let X be SubRealNormSpace of V; :: thesis: for f being Lipschitzian linear-Functional of X
for F being Point of (DualSp X) st f = F & ( for x being VECTOR of X
for v being VECTOR of V st x = v holds
f . x <= ||.v.|| ) holds
ex g being Lipschitzian linear-Functional of V ex G being Point of (DualSp V) st
( g = G & g | the carrier of X = f & ( for x being VECTOR of V holds
( g . x <= ||.x.|| & ||.G.|| = ||.F.|| ) ) )
let f be Lipschitzian linear-Functional of X; :: thesis: for F being Point of (DualSp X) st f = F & ( for x being VECTOR of X
for v being VECTOR of V st x = v holds
f . x <= ||.v.|| ) holds
ex g being Lipschitzian linear-Functional of V ex G being Point of (DualSp V) st
( g = G & g | the carrier of X = f & ( for x being VECTOR of V holds
( g . x <= ||.x.|| & ||.G.|| = ||.F.|| ) ) )
let F be Point of (DualSp X); :: thesis: ( f = F & ( for x being VECTOR of X
for v being VECTOR of V st x = v holds
f . x <= ||.v.|| ) implies ex g being Lipschitzian linear-Functional of V ex G being Point of (DualSp V) st
( g = G & g | the carrier of X = f & ( for x being VECTOR of V holds
( g . x <= ||.x.|| & ||.G.|| = ||.F.|| ) ) ) )
assume that
A11: f = F and
A12: for x being VECTOR of X
for v being VECTOR of V st x = v holds
f . x <= ||.v.|| ; :: thesis: ex g being Lipschitzian linear-Functional of V ex G being Point of (DualSp V) st
( g = G & g | the carrier of X = f & ( for x being VECTOR of V holds
( g . x <= ||.x.|| & ||.G.|| = ||.F.|| ) ) )
consider g being Lipschitzian linear-Functional of V, G being Point of (DualSp V) such that
A2: ( g = G & g | the carrier of X = f & ||.G.|| = ||.F.|| ) by A11, Th44;
reconsider X0 = X as RealLinearSpace ;
B1: ( the carrier of X0 c= the carrier of V & 0. X0 = 0. V & the addF of X0 = the addF of V || the carrier of X0 & the Mult of X0 = the Mult of V | [:REAL, the carrier of X0:] ) by DefSubSP;

now :: thesis: for r being Real st r in PreNorms f holds
r <= 1

let r be Real; :: thesis: ( r in PreNorms f implies r <= 1 )
assume r in PreNorms f ; :: thesis: r <= 1
then consider t being VECTOR of X such that
C1: ( r = |.(f . t).| & ||.t.|| <= 1 ) ;
reconsider td = t as VECTOR of V by B1;
C7: ||.t.|| = ( the normF of V | the carrier of X) . td by DefSubSP
.= ||.td.|| by FUNCT_1:49 ;
C5: - (f . t) = (- 1) * (f . t)
.= f . ((- 1) * t) by HAHNBAN:def 3 ;
reconsider t0 = t as VECTOR of X0 ;
D6: X0 is Subspace of V by B1, RLSUB_1:def 2;
( (- 1) * td = - td & (- 1) * t = - t ) by RLVECT_1:16;
then (- 1) * td = (- 1) * t by RLSUB_1:15, D6;
then f . ((- 1) * t) <= ||.((- 1) * td).|| by A12;
then f . ((- 1) * t) <= ||.(- td).|| by RLVECT_1:16;
then - (f . t) <= ||.td.|| by C5, NORMSP_1:2;
then - ||.td.|| <= f . t by XREAL_1:26;
then |.(f . t).| <= ||.td.|| by A12, ABSVALUE:5;
hence r <= 1 by C1, C7, XXREAL_0:2; :: thesis: verum

end;

then upper_bound (PreNorms f) <= 1 by SEQ_4:45;
then A3: ||.G.|| <= 1 by A2, A11, Th30;
for x being VECTOR of V holds g . x <= ||.x.||

proof

let x be VECTOR of V; :: thesis: g . x <= ||.x.||
C1: g . x <= |.(g . x).| by ABSVALUE:4;
|.(g . x).| <= ||.G.|| * ||.x.|| by A2, Th32;
then C2: g . x <= ||.G.|| * ||.x.|| by C1, XXREAL_0:2;
||.G.|| * ||.x.|| <= 1 * ||.x.|| by A3, XREAL_1:64;
hence g . x <= ||.x.|| by C2, XXREAL_0:2; :: thesis: verum

end;

hence ex g being Lipschitzian linear-Functional of V ex G being Point of (DualSp V) st
( g = G & g | the carrier of X = f & ( for x being VECTOR of V holds
( g . x <= ||.x.|| & ||.G.|| = ||.F.|| ) ) ) by A2; :: thesis: verum