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 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 & ||.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 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 & ||.G.|| = ||.F.|| )

let f be Lipschitzian linear-Functional of X; :: thesis: for F being Point of (DualSp X) st f = F 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 & ||.G.|| = ||.F.|| )

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

assume A1: f = F ; :: 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 & ||.G.|| = ||.F.|| )

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 reconsider X0 = X0 as Subspace of V by RLSUB_1:def 2;

reconsider fi0 = f as linear-Functional of X0 ;

deffunc H_{1}( Element of the carrier of V) -> set = ||.F.|| * ||.$1.||;

D0: for v being Element of the carrier of V holds H_{1}(v) in REAL
by XREAL_0:def 1;

consider q being Function of the carrier of V,REAL such that

D1: for v being Element of the carrier of V holds q . v = H_{1}(v)
from FUNCT_2:sch 8(D0);

q is Banach-Functional of V

for x being VECTOR of X0

for v being VECTOR of V st x = v holds

fi0 . x <= q . v

A3: ( g | the carrier of X0 = fi0 & ( for x being VECTOR of V holds g . x <= q . x ) ) by HAHNBAN:22;

B4: for x being VECTOR of V holds |.(g . x).| <= ||.F.|| * ||.x.||

reconsider G = g as Point of (DualSp V) by Def9;

then A41: (BoundedLinearFunctionalsNorm V) . g <= (BoundedLinearFunctionalsNorm X) . f by Th30;

upper_bound (PreNorms f) <= upper_bound (PreNorms g) by A42, SEQ_4:48;

then (BoundedLinearFunctionalsNorm X) . f <= upper_bound (PreNorms g) by Th30;

then B4: (BoundedLinearFunctionalsNorm X) . f <= (BoundedLinearFunctionalsNorm V) . g by Th30;

take g ; :: thesis: ex G being Point of (DualSp V) st

( g = G & g | the carrier of X = f & ||.G.|| = ||.F.|| )

take G ; :: thesis: ( g = G & g | the carrier of X = f & ||.G.|| = ||.F.|| )

thus ( g = G & g | the carrier of X = f & ||.G.|| = ||.F.|| ) by A3, A1, A41, XXREAL_0:1, B4; :: thesis: verum

for f being Lipschitzian linear-Functional of X

for F being Point of (DualSp X) st f = F 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 & ||.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 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 & ||.G.|| = ||.F.|| )

let f be Lipschitzian linear-Functional of X; :: thesis: for F being Point of (DualSp X) st f = F 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 & ||.G.|| = ||.F.|| )

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

assume A1: f = F ; :: 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 & ||.G.|| = ||.F.|| )

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 reconsider X0 = X0 as Subspace of V by RLSUB_1:def 2;

reconsider fi0 = f as linear-Functional of X0 ;

deffunc H

D0: for v being Element of the carrier of V holds H

consider q being Function of the carrier of V,REAL such that

D1: for v being Element of the carrier of V holds q . v = H

q is Banach-Functional of V

proof

then reconsider q = q as Banach-Functional of V ;
E0:
q is subadditive

end;proof

q is absolutely_homogeneous
let x, y be VECTOR of V; :: according to HAHNBAN:def 1 :: thesis: q . (x + y) <= K55((q . x),(q . y))

E2: ( q . x = ||.F.|| * ||.x.|| & q . y = ||.F.|| * ||.y.|| ) by D1;

||.F.|| * ||.(x + y).|| <= ||.F.|| * (||.x.|| + ||.y.||) by XREAL_1:64, NORMSP_1:def 1;

hence q . (x + y) <= K55((q . x),(q . y)) by D1, E2; :: thesis: verum

end;E2: ( q . x = ||.F.|| * ||.x.|| & q . y = ||.F.|| * ||.y.|| ) by D1;

||.F.|| * ||.(x + y).|| <= ||.F.|| * (||.x.|| + ||.y.||) by XREAL_1:64, NORMSP_1:def 1;

hence q . (x + y) <= K55((q . x),(q . y)) by D1, E2; :: thesis: verum

proof

hence
q is Banach-Functional of V
by E0; :: thesis: verum
let x be VECTOR of V; :: according to HAHNBAN:def 6 :: thesis: for b_{1} being object holds q . (b_{1} * x) = |.b_{1}.| * (q . x)

let r be Real; :: thesis: q . (r * x) = |.r.| * (q . x)

E5: ||.(r * x).|| = |.r.| * ||.x.|| by NORMSP_1:def 1;

q . (r * x) = ||.F.|| * ||.(r * x).|| by D1

.= |.r.| * (||.F.|| * ||.x.||) by E5 ;

hence q . (r * x) = |.r.| * (q . x) by D1; :: thesis: verum

end;let r be Real; :: thesis: q . (r * x) = |.r.| * (q . x)

E5: ||.(r * x).|| = |.r.| * ||.x.|| by NORMSP_1:def 1;

q . (r * x) = ||.F.|| * ||.(r * x).|| by D1

.= |.r.| * (||.F.|| * ||.x.||) by E5 ;

hence q . (r * x) = |.r.| * (q . x) by D1; :: thesis: verum

for x being VECTOR of X0

for v being VECTOR of V st x = v holds

fi0 . x <= q . v

proof

then consider g being linear-Functional of V such that
let x0 be VECTOR of X0; :: thesis: for v being VECTOR of V st x0 = v holds

fi0 . x0 <= q . v

let v be VECTOR of V; :: thesis: ( x0 = v implies fi0 . x0 <= q . v )

assume D21: x0 = v ; :: thesis: fi0 . x0 <= q . v

reconsider x = x0 as VECTOR of X ;

D22: fi0 . x0 <= |.(fi0 . x0).| by ABSVALUE:4;

D23: |.(fi0 . x).| <= ||.F.|| * ||.x.|| by A1, Th32;

||.x.|| = ( the normF of V | the carrier of X) . v by D21, DefSubSP

.= ||.v.|| by FUNCT_1:49, D21 ;

then |.(fi0 . x0).| <= q . v by D1, D23;

hence fi0 . x0 <= q . v by D22, XXREAL_0:2; :: thesis: verum

end;fi0 . x0 <= q . v

let v be VECTOR of V; :: thesis: ( x0 = v implies fi0 . x0 <= q . v )

assume D21: x0 = v ; :: thesis: fi0 . x0 <= q . v

reconsider x = x0 as VECTOR of X ;

D22: fi0 . x0 <= |.(fi0 . x0).| by ABSVALUE:4;

D23: |.(fi0 . x).| <= ||.F.|| * ||.x.|| by A1, Th32;

||.x.|| = ( the normF of V | the carrier of X) . v by D21, DefSubSP

.= ||.v.|| by FUNCT_1:49, D21 ;

then |.(fi0 . x0).| <= q . v by D1, D23;

hence fi0 . x0 <= q . v by D22, XXREAL_0:2; :: thesis: verum

A3: ( g | the carrier of X0 = fi0 & ( for x being VECTOR of V holds g . x <= q . x ) ) by HAHNBAN:22;

B4: for x being VECTOR of V holds |.(g . x).| <= ||.F.|| * ||.x.||

proof

then reconsider g = g as Lipschitzian linear-Functional of V by Def8;
let x be VECTOR of V; :: thesis: |.(g . x).| <= ||.F.|| * ||.x.||

g . x <= q . x by A3;

then A31: g . x <= ||.F.|| * ||.x.|| by D1;

A32: - (g . x) = (- 1) * (g . x)

.= g . ((- 1) * x) by HAHNBAN:def 3 ;

g . ((- 1) * x) <= q . ((- 1) * x) by A3;

then g . ((- 1) * x) <= ||.F.|| * ||.((- 1) * x).|| by D1;

then g . ((- 1) * x) <= ||.F.|| * ||.(- x).|| by RLVECT_1:16;

then - (g . x) <= ||.F.|| * ||.x.|| by A32, NORMSP_1:2;

then - (||.F.|| * ||.x.||) <= g . x by XREAL_1:26;

hence |.(g . x).| <= ||.F.|| * ||.x.|| by ABSVALUE:5, A31; :: thesis: verum

end;g . x <= q . x by A3;

then A31: g . x <= ||.F.|| * ||.x.|| by D1;

A32: - (g . x) = (- 1) * (g . x)

.= g . ((- 1) * x) by HAHNBAN:def 3 ;

g . ((- 1) * x) <= q . ((- 1) * x) by A3;

then g . ((- 1) * x) <= ||.F.|| * ||.((- 1) * x).|| by D1;

then g . ((- 1) * x) <= ||.F.|| * ||.(- x).|| by RLVECT_1:16;

then - (g . x) <= ||.F.|| * ||.x.|| by A32, NORMSP_1:2;

then - (||.F.|| * ||.x.||) <= g . x by XREAL_1:26;

hence |.(g . x).| <= ||.F.|| * ||.x.|| by ABSVALUE:5, A31; :: thesis: verum

reconsider G = g as Point of (DualSp V) by Def9;

now :: thesis: for r being Real st r in PreNorms g holds

r <= ||.F.||

then
upper_bound (PreNorms g) <= (BoundedLinearFunctionalsNorm X) . f
by A1, SEQ_4:45;r <= ||.F.||

let r be Real; :: thesis: ( r in PreNorms g implies r <= ||.F.|| )

assume r in PreNorms g ; :: thesis: r <= ||.F.||

then consider t being VECTOR of V such that

C1: r = |.(g . t).| and

C2: ||.t.|| <= 1 ;

C3: |.(g . t).| <= ||.F.|| * ||.t.|| by B4;

||.F.|| * ||.t.|| <= ||.F.|| * 1 by C2, XREAL_1:64;

hence r <= ||.F.|| by C1, C3, XXREAL_0:2; :: thesis: verum

end;assume r in PreNorms g ; :: thesis: r <= ||.F.||

then consider t being VECTOR of V such that

C1: r = |.(g . t).| and

C2: ||.t.|| <= 1 ;

C3: |.(g . t).| <= ||.F.|| * ||.t.|| by B4;

||.F.|| * ||.t.|| <= ||.F.|| * 1 by C2, XREAL_1:64;

hence r <= ||.F.|| by C1, C3, XXREAL_0:2; :: thesis: verum

then A41: (BoundedLinearFunctionalsNorm V) . g <= (BoundedLinearFunctionalsNorm X) . f by Th30;

now :: thesis: for r being object st r in PreNorms f holds

r in PreNorms g

then A42:
PreNorms f c= PreNorms g
;r in PreNorms g

let r be object ; :: thesis: ( r in PreNorms f implies r in PreNorms g )

assume r in PreNorms f ; :: thesis: r in PreNorms g

then consider t being VECTOR of X such that

C1: r = |.(f . t).| and

C2: ||.t.|| <= 1 ;

reconsider td = t as VECTOR of V by B1;

||.t.|| = ( the normF of V | the carrier of X) . td by DefSubSP

.= ||.td.|| by FUNCT_1:49 ;

then ( r = |.(g . td).| & ||.td.|| <= 1 ) by C1, A3, FUNCT_1:49, C2;

hence r in PreNorms g ; :: thesis: verum

end;assume r in PreNorms f ; :: thesis: r in PreNorms g

then consider t being VECTOR of X such that

C1: r = |.(f . t).| and

C2: ||.t.|| <= 1 ;

reconsider td = t as VECTOR of V by B1;

||.t.|| = ( the normF of V | the carrier of X) . td by DefSubSP

.= ||.td.|| by FUNCT_1:49 ;

then ( r = |.(g . td).| & ||.td.|| <= 1 ) by C1, A3, FUNCT_1:49, C2;

hence r in PreNorms g ; :: thesis: verum

upper_bound (PreNorms f) <= upper_bound (PreNorms g) by A42, SEQ_4:48;

then (BoundedLinearFunctionalsNorm X) . f <= upper_bound (PreNorms g) by Th30;

then B4: (BoundedLinearFunctionalsNorm X) . f <= (BoundedLinearFunctionalsNorm V) . g by Th30;

take g ; :: thesis: ex G being Point of (DualSp V) st

( g = G & g | the carrier of X = f & ||.G.|| = ||.F.|| )

take G ; :: thesis: ( g = G & g | the carrier of X = f & ||.G.|| = ||.F.|| )

thus ( g = G & g | the carrier of X = f & ||.G.|| = ||.F.|| ) by A3, A1, A41, XXREAL_0:1, B4; :: thesis: verum