let V be RealNormSpace; for x0 being Point of V st x0 <> 0. V holds
ex G being Point of (DualSp V) st
( (Bound2Lipschitz (G,V)) . x0 = 1 & ||.G.|| = 1 / ||.x0.|| )
let x0 be Point of V; ( x0 <> 0. V implies ex G being Point of (DualSp V) st
( (Bound2Lipschitz (G,V)) . x0 = 1 & ||.G.|| = 1 / ||.x0.|| ) )
assume AS0:
x0 <> 0. V
; ex G being Point of (DualSp V) st
( (Bound2Lipschitz (G,V)) . x0 = 1 & ||.G.|| = 1 / ||.x0.|| )
set X = NLin {(0. V)};
set Y = the carrier of (Lin {(0. V)});
for s being object holds
( s in the carrier of (Lin {(0. V)}) iff s in {(0. V)} )
then Y1:
the carrier of (NLin {(0. V)}) = {(0. V)}
by TARSKI:2;
set Z = { ||.(x - x0).|| where x is Point of V : x in NLin {(0. V)} } ;
Y2:
for s being object holds
( s in { ||.(x - x0).|| where x is Point of V : x in NLin {(0. V)} } iff s in {||.x0.||} )
then reconsider Z = { ||.(x - x0).|| where x is Point of V : x in NLin {(0. V)} } as non empty Subset of REAL by TARSKI:2;
reconsider d = lower_bound Z as Real ;
Y3:
Z = {||.x0.||}
by Y2;
then X4:
d = ||.x0.||
by SEQ_4:9;
then
d <> 0
by AS0, NORMSP_0:def 5;
then consider G being Point of (DualSp V) such that
X3:
( ( for x being Point of V st x in NLin {(0. V)} holds
(Bound2Lipschitz (G,V)) . x = 0 ) & (Bound2Lipschitz (G,V)) . x0 = 1 & ||.G.|| = 1 / d )
by X4, Th63;
take
G
; ( (Bound2Lipschitz (G,V)) . x0 = 1 & ||.G.|| = 1 / ||.x0.|| )
thus
( (Bound2Lipschitz (G,V)) . x0 = 1 & ||.G.|| = 1 / ||.x0.|| )
by X3, SEQ_4:9, Y3; verum