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;

then A3: ||.G.|| <= 1 by A2, A11, Th30;

for x being VECTOR of V holds g . x <= ||.x.||

( g = G & g | the carrier of X = f & ( for x being VECTOR of V holds

( g . x <= ||.x.|| & ||.G.|| = ||.F.|| ) ) ) by A2; :: thesis: verum

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

then
upper_bound (PreNorms f) <= 1
by SEQ_4:45;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;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

then A3: ||.G.|| <= 1 by A2, A11, Th30;

for x being VECTOR of V holds g . x <= ||.x.||

proof

hence
ex g being Lipschitzian linear-Functional of V ex G being Point of (DualSp V) st
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;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

( g = G & g | the carrier of X = f & ( for x being VECTOR of V holds

( g . x <= ||.x.|| & ||.G.|| = ||.F.|| ) ) ) by A2; :: thesis: verum