let V be RealNormSpace; :: thesis: for X being SubRealNormSpace of V
for f being Lipschitzian linear-Functional of X
for F being Point of () st f = F holds
ex g being Lipschitzian linear-Functional of V ex G being Point of () st
( g = G & g | the carrier of X = f & = )

let X be SubRealNormSpace of V; :: thesis: for f being Lipschitzian linear-Functional of X
for F being Point of () st f = F holds
ex g being Lipschitzian linear-Functional of V ex G being Point of () st
( g = G & g | the carrier of X = f & = )

let f be Lipschitzian linear-Functional of X; :: thesis: for F being Point of () st f = F holds
ex g being Lipschitzian linear-Functional of V ex G being Point of () st
( g = G & g | the carrier of X = f & = )

let F be Point of (); :: thesis: ( f = F implies ex g being Lipschitzian linear-Functional of V ex G being Point of () st
( g = G & g | the carrier of X = f & = ) )

assume A1: f = F ; :: thesis: ex g being Lipschitzian linear-Functional of V ex G being Point of () st
( g = G & g | the carrier of X = 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 H1( Element of the carrier of V) -> set = * ||.\$1.||;
D0: for v being Element of the carrier of V holds H1(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 = H1(v) from 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 = * & q . y = * ) by D1;
||.F.|| * ||.(x + y).|| <= * () by ;
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 b1 being object holds q . (b1 * x) = |.b1.| * (q . x)
let r be Real; :: thesis: q . (r * x) = |.r.| * (q . x)
E5: ||.(r * x).|| = |.r.| * by NORMSP_1:def 1;
q . (r * x) = * ||.(r * x).|| by D1
.= |.r.| * () 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).| <= * by ;
= ( the normF of V | the carrier of X) . v by
.= by ;
then |.(fi0 . x0).| <= q . v by ;
hence fi0 . x0 <= q . v by ; :: 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).| <= *
proof
let x be VECTOR of V; :: thesis: |.(g . x).| <= *
g . x <= q . x by A3;
then A31: g . 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) <= * ||.((- 1) * x).|| by D1;
then g . ((- 1) * x) <= * ||.(- x).|| by RLVECT_1:16;
then - (g . x) <= * by ;
then - () <= g . x by XREAL_1:26;
hence |.(g . x).| <= * by ; :: thesis: verum
end;
then reconsider g = g as Lipschitzian linear-Functional of V by Def8;
reconsider G = g as Point of () by Def9;
now :: thesis: for r being Real st r in PreNorms g holds
r <=
let r be Real; :: thesis: ( r in PreNorms g implies r <= )
assume r in PreNorms g ; :: thesis: r <=
then consider t being VECTOR of V such that
C1: r = |.(g . t).| and
C2: ||.t.|| <= 1 ;
C3: |.(g . t).| <= * by B4;
||.F.|| * <= * 1 by ;
hence r <= by ; :: thesis: verum
end;
then upper_bound () <= . f by ;
then A41: (BoundedLinearFunctionalsNorm V) . g <= . 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:
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;
= ( the normF of V | the carrier of X) . td by DefSubSP
.= ||.td.|| by FUNCT_1:49 ;
then ( r = |.(g . td).| & ||.td.|| <= 1 ) by ;
hence r in PreNorms g ; :: thesis: verum
end;
then A42: PreNorms f c= PreNorms g ;
upper_bound () <= upper_bound () by ;
then (BoundedLinearFunctionalsNorm X) . f <= upper_bound () by Th30;
then B4: (BoundedLinearFunctionalsNorm X) . f <= . g by Th30;
take g ; :: thesis: ex G being Point of () st
( g = G & g | the carrier of X = f & = )

take G ; :: thesis: ( g = G & g | the carrier of X = f & = )
thus ( g = G & g | the carrier of X = f & = ) by ; :: thesis: verum