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 & ( for x being VECTOR of X
for v being VECTOR of V st x = v holds
f . x <= ) holds
ex g being Lipschitzian linear-Functional of V ex G being Point of () st
( g = G & g | the carrier of X = f & ( for x being VECTOR of V holds
( g . x <= & = ) ) )

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

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

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

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 <= ; :: thesis: ex g being Lipschitzian linear-Functional of V ex G being Point of () st
( g = G & g | the carrier of X = f & ( for x being VECTOR of V holds
( g . x <= & = ) ) )

consider g being Lipschitzian linear-Functional of V, G being Point of () such that
A2: ( g = G & g | the carrier of X = f & = ) by ;
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).| & <= 1 ) ;
reconsider td = t as VECTOR of V by B1;
C7: = ( 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 ;
( (- 1) * td = - td & (- 1) * t = - t ) by RLVECT_1:16;
then (- 1) * td = (- 1) * t by ;
then f . ((- 1) * t) <= ||.((- 1) * td).|| by A12;
then f . ((- 1) * t) <= ||.(- td).|| by RLVECT_1:16;
then - (f . t) <= ||.td.|| by ;
then - ||.td.|| <= f . t by XREAL_1:26;
then |.(f . t).| <= ||.td.|| by ;
hence r <= 1 by ; :: thesis: verum
end;
then upper_bound () <= 1 by SEQ_4:45;
then A3: ||.G.|| <= 1 by ;
for x being VECTOR of V holds g . x <=
proof
let x be VECTOR of V; :: thesis: g . x <=
C1: g . x <= |.(g . x).| by ABSVALUE:4;
|.(g . x).| <= * by ;
then C2: g . x <= * by ;
||.G.|| * <= 1 * by ;
hence g . x <= by ; :: thesis: verum
end;
hence ex g being Lipschitzian linear-Functional of V ex G being Point of () st
( g = G & g | the carrier of X = f & ( for x being VECTOR of V holds
( g . x <= & = ) ) ) by A2; :: thesis: verum