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₁( Element of the carrier of V) -> set = ||.F.|| * ||.$1.||;
D0: for v being Element of the carrier of V holds H₁(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₁(v) from FUNCT_2:sch 8(D0);
q is Banach-Functional of V

proof

E0: q is subadditive

proof

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;

q is absolutely_homogeneous

proof

let x be VECTOR of V; :: according to HAHNBAN:def 6 :: thesis: for b₁ being object holds q . (b₁ * x) = |.b₁.| * (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;

hence q is Banach-Functional of V by E0; :: thesis: verum

end;

then reconsider q = q as Banach-Functional of V ;
for x being VECTOR of X0
for v being VECTOR of V st x = v holds
fi0 . x <= q . v

proof

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;

then consider g being linear-Functional of V such that
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

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;

then reconsider g = g as Lipschitzian linear-Functional of V by Def8;
reconsider G = g as Point of (DualSp V) by Def9;

now :: thesis: for r being Real st r in PreNorms g holds
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;

then upper_bound (PreNorms g) <= (BoundedLinearFunctionalsNorm X) . f by A1, SEQ_4:45;
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

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;

then A42: PreNorms f c= PreNorms g ;
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