let V be RealNormSpace; :: thesis: for X being SubRealNormSpace of V
for x0 being Point of V
for d being Real st ex Z being non empty Subset of REAL st
( Z = { ||.(x - x0).|| where x is Point of V : x in X } & d = lower_bound Z & lower_bound Z > 0 ) holds
( not x0 in X & ex G being Point of (DualSp V) st
( ( for x being Point of V st x in X holds
(Bound2Lipschitz (G,V)) . x = 0 ) & (Bound2Lipschitz (G,V)) . x0 = 1 & ||.G.|| = 1 / d ) )
let X be SubRealNormSpace of V; :: thesis: for x0 being Point of V
for d being Real st ex Z being non empty Subset of REAL st
( Z = { ||.(x - x0).|| where x is Point of V : x in X } & d = lower_bound Z & lower_bound Z > 0 ) holds
( not x0 in X & ex G being Point of (DualSp V) st
( ( for x being Point of V st x in X holds
(Bound2Lipschitz (G,V)) . x = 0 ) & (Bound2Lipschitz (G,V)) . x0 = 1 & ||.G.|| = 1 / d ) )
let x0 be Point of V; :: thesis: for d being Real st ex Z being non empty Subset of REAL st
( Z = { ||.(x - x0).|| where x is Point of V : x in X } & d = lower_bound Z & lower_bound Z > 0 ) holds
( not x0 in X & ex G being Point of (DualSp V) st
( ( for x being Point of V st x in X holds
(Bound2Lipschitz (G,V)) . x = 0 ) & (Bound2Lipschitz (G,V)) . x0 = 1 & ||.G.|| = 1 / d ) )
let d be Real; :: thesis: ( ex Z being non empty Subset of REAL st
( Z = { ||.(x - x0).|| where x is Point of V : x in X } & d = lower_bound Z & lower_bound Z > 0 ) implies ( not x0 in X & ex G being Point of (DualSp V) st
( ( for x being Point of V st x in X holds
(Bound2Lipschitz (G,V)) . x = 0 ) & (Bound2Lipschitz (G,V)) . x0 = 1 & ||.G.|| = 1 / d ) ) )
assume ex Z being non empty Subset of REAL st
( Z = { ||.(x - x0).|| where x is Point of V : x in X } & d = lower_bound Z & lower_bound Z > 0 ) ; :: thesis: ( not x0 in X & ex G being Point of (DualSp V) st
( ( for x being Point of V st x in X holds
(Bound2Lipschitz (G,V)) . x = 0 ) & (Bound2Lipschitz (G,V)) . x0 = 1 & ||.G.|| = 1 / d ) )
then consider Z being non empty Subset of REAL such that
AS2: ( Z = { ||.(x - x0).|| where x is Point of V : x in X } & d = lower_bound Z & lower_bound Z > 0 ) ;
set M0 = { (z + (a * x0)) where z is Point of V, a is Real : z in X } ;
A1: 0. V = (0. V) + (0 * x0) by RLVECT_1:10;
0. V = 0. X by DUALSP01:def 16;
then D1: 0. V in X ;
then 0. V in { (z + (a * x0)) where z is Point of V, a is Real : z in X } by A1;
then reconsider M0 = { (z + (a * x0)) where z is Point of V, a is Real : z in X } as non empty set ;

now :: thesis: for x being object st x in M0 holds
x in the carrier of V

let x be object ; :: thesis: ( x in M0 implies x in the carrier of V )
assume x in M0 ; :: thesis: x in the carrier of V
then ex z being Point of V ex a being Real st
( x = z + (a * x0) & z in X ) ;
hence x in the carrier of V ; :: thesis: verum

end;

then M0 c= the carrier of V ;
then reconsider M0 = M0 as non empty Subset of V ;
B0: X is Subspace of V by NORMSP_3:27;
set M = NLin M0;
AD1: M0 is linearly-closed

proof

A0: for v, u being VECTOR of V st v in M0 & u in M0 holds
v + u in M0

proof

let v, u be VECTOR of V; :: thesis: ( v in M0 & u in M0 implies v + u in M0 )
assume A1: ( v in M0 & u in M0 ) ; :: thesis: v + u in M0
then consider z1 being Point of V, a being Real such that
A3: ( v = z1 + (a * x0) & z1 in X ) ;
consider z2 being Point of V, b being Real such that
A5: ( u = z2 + (b * x0) & z2 in X ) by A1;
A7: v + u = z1 + ((a * x0) + (z2 + (b * x0))) by A3, A5, RLVECT_1:def 3
.= z1 + (z2 + ((a * x0) + (b * x0))) by RLVECT_1:def 3
.= (z1 + z2) + ((a * x0) + (b * x0)) by RLVECT_1:def 3
.= (z1 + z2) + ((a + b) * x0) by RLVECT_1:def 6 ;
z1 + z2 in X by B0, A3, A5, RLSUB_1:20;
hence v + u in M0 by A7; :: thesis: verum

end;

for r being Real
for v being VECTOR of V st v in M0 holds
r * v in M0

proof

let r be Real; :: thesis: for v being VECTOR of V st v in M0 holds
r * v in M0
let v be VECTOR of V; :: thesis: ( v in M0 implies r * v in M0 )
assume v in M0 ; :: thesis: r * v in M0
then consider z being Point of V, a being Real such that
A9: ( v = z + (a * x0) & z in X ) ;
A11: r * v = (r * z) + (r * (a * x0)) by A9, RLVECT_1:def 5
.= (r * z) + ((r * a) * x0) by RLVECT_1:def 7 ;
r * z in X by B0, A9, RLSUB_1:21;
hence r * v in M0 by A11; :: thesis: verum

end;

hence M0 is linearly-closed by A0; :: thesis: verum

end;

then X01: the carrier of (NLin M0) = M0 by NORMSP_3:31;
V2: x0 = (0. V) + (1 * x0) by RLVECT_1:def 8;
then V21: x0 in NLin M0 by D1, X01;
AD2: for v being Point of (NLin M0) ex x being Point of V ex a being Real st
( v = x + (a * x0) & x in X )

proof

let v be Point of (NLin M0); :: thesis: ex x being Point of V ex a being Real st
( v = x + (a * x0) & x in X )
v in the carrier of (Lin M0) ;
then v in M0 by AD1, NORMSP_3:31;
hence ex x being Point of V ex a being Real st
( v = x + (a * x0) & x in X ) ; :: thesis: verum

end;

reconsider r0 = 0 as Real ;
for r being ExtReal st r in Z holds
r0 <= r

proof

let r be ExtReal; :: thesis: ( r in Z implies r0 <= r )
assume r in Z ; :: thesis: r0 <= r
then ex x being Point of V st
( r = ||.(x - x0).|| & x in X ) by AS2;
hence r0 <= r ; :: thesis: verum

end;

then r0 is LowerBound of Z by XXREAL_2:def 2;
then U2: Z is bounded_below ;

P4: now :: thesis: not x0 in X

assume Q1: x0 in X ; :: thesis: contradiction
reconsider x0 = x0 as Point of V ;
||.(x0 - x0).|| = ||.(0. V).|| by RLVECT_1:15;
then r0 in Z by Q1, AS2;
hence contradiction by AS2, U2, SEQ_4:def 2; :: thesis: verum

end;

hence not x0 in X ; :: thesis: ex G being Point of (DualSp V) st
( ( for x being Point of V st x in X holds
(Bound2Lipschitz (G,V)) . x = 0 ) & (Bound2Lipschitz (G,V)) . x0 = 1 & ||.G.|| = 1 / d )
AD3: for x1, x2 being Point of V
for a1, a2 being Real st x1 in X & x2 in X & x1 + (a1 * x0) = x2 + (a2 * x0) holds
( x1 = x2 & a1 = a2 )

proof

let x1, x2 be Point of V; :: thesis: for a1, a2 being Real st x1 in X & x2 in X & x1 + (a1 * x0) = x2 + (a2 * x0) holds
( x1 = x2 & a1 = a2 )
let a1, a2 be Real; :: thesis: ( x1 in X & x2 in X & x1 + (a1 * x0) = x2 + (a2 * x0) implies ( x1 = x2 & a1 = a2 ) )
assume P1: ( x1 in X & x2 in X & x1 + (a1 * x0) = x2 + (a2 * x0) ) ; :: thesis: ( x1 = x2 & a1 = a2 )
then (x1 + (a1 * x0)) - x2 = (x2 + (- x2)) + (a2 * x0) by RLVECT_1:def 3
.= (0. V) + (a2 * x0) by RLVECT_1:5 ;
then P5: ((x1 + (a1 * x0)) - x2) - (a1 * x0) = (a2 - a1) * x0 by RLVECT_1:35;
P6: ((x1 + (a1 * x0)) - x2) - (a1 * x0) = (x1 + (a1 * x0)) + ((- x2) - (a1 * x0)) by RLVECT_1:def 3
.= x1 + ((a1 * x0) + ((- x2) - (a1 * x0))) by RLVECT_1:def 3
.= x1 + (((a1 * x0) + (- x2)) - (a1 * x0)) by RLVECT_1:def 3
.= x1 + ((- x2) + ((a1 * x0) - (a1 * x0))) by RLVECT_1:def 3
.= x1 + ((- x2) + (0. V)) by RLVECT_1:15 ;
P7: a2 = a1

proof

assume a2 <> a1 ; :: thesis: contradiction
then Q0: a2 - a1 <> 0 ;
then Q1: (a2 - a1) * (1 / (a2 - a1)) = 1 by XCMPLX_1:106;
1 * (x1 - x2) = (a2 - a1) * x0 by P5, P6, RLVECT_1:def 8;
then (a2 - a1) * ((1 / (a2 - a1)) * (x1 - x2)) = (a2 - a1) * x0 by Q1, RLVECT_1:def 7;
then Q2: (1 / (a2 - a1)) * (x1 - x2) = x0 by Q0, RLVECT_1:36;
reconsider r = 1 / (a2 - a1) as Real ;
Q4: ( r * x1 in X & r * x2 in X ) by B0, P1, RLSUB_1:21;
r * (x1 - x2) = (r * x1) - (r * x2) by RLVECT_1:34;
hence contradiction by P4, Q2, B0, Q4, RLSUB_1:23; :: thesis: verum

end;

then x1 - x2 = 0. V by P5, P6, RLVECT_1:10;
hence ( x1 = x2 & a1 = a2 ) by P7, RLVECT_1:21; :: thesis: verum

end;

defpred S₁[ object , object ] means ex z being Point of V ex a being Real st
( z in X & $1 = z + (a * x0) & $2 = a );
F1: for v being Element of (NLin M0) ex a being Element of REAL st S₁[v,a]

proof

let v be Element of (NLin M0); :: thesis: ex a being Element of REAL st S₁[v,a]
consider z being Point of V, a being Real such that
B0: ( v = z + (a * x0) & z in X ) by AD2;
reconsider aa = a as Element of REAL by XREAL_0:def 1;
take aa ; :: thesis: S₁[v,aa]
thus S₁[v,aa] by B0; :: thesis: verum

end;

consider f being Function of (NLin M0),REAL such that
A1F: for x being Element of (NLin M0) holds S₁[x,f . x] from FUNCT_2:sch 3(F1);
A1: for v being Point of (NLin M0)
for z being Point of V
for a being Real st z in X & v = z + (a * x0) holds
f . v = a

proof

let v be Point of (NLin M0); :: thesis: for z being Point of V
for a being Real st z in X & v = z + (a * x0) holds
f . v = a
let z be Point of V; :: thesis: for a being Real st z in X & v = z + (a * x0) holds
f . v = a
let a be Real; :: thesis: ( z in X & v = z + (a * x0) implies f . v = a )
assume AS0: ( z in X & v = z + (a * x0) ) ; :: thesis: f . v = a
ex z1 being Point of V ex a1 being Real st
( z1 in X & v = z1 + (a1 * x0) & f . v = a1 ) by A1F;
hence f . v = a by AS0, AD3; :: thesis: verum

end;

f is linear-Functional of (NLin M0)

proof

B1: f is additive

proof

let v, w be VECTOR of (NLin M0); :: according to HAHNBAN:def 2 :: thesis: f . (v + w) = (f . v) + (f . w)
consider x1 being Point of V, a1 being Real such that
B11: ( v = x1 + (a1 * x0) & x1 in X ) by AD2;
consider x2 being Point of V, a2 being Real such that
B13: ( w = x2 + (a2 * x0) & x2 in X ) by AD2;
B14: ( f . v = a1 & f . w = a2 ) by A1, B11, B13;
v + w = (x1 + (a1 * x0)) + (x2 + (a2 * x0)) by B11, B13, NORMSP_3:28
.= x1 + ((a1 * x0) + (x2 + (a2 * x0))) by RLVECT_1:def 3
.= x1 + (x2 + ((a1 * x0) + (a2 * x0))) by RLVECT_1:def 3
.= (x1 + x2) + ((a1 * x0) + (a2 * x0)) by RLVECT_1:def 3
.= (x1 + x2) + ((a1 + a2) * x0) by RLVECT_1:def 6 ;
hence f . (v + w) = (f . v) + (f . w) by B14, A1, B0, B11, B13, RLSUB_1:20; :: thesis: verum

end;

f is homogeneous

proof

let v be VECTOR of (NLin M0); :: according to HAHNBAN:def 3 :: thesis: for b₁ being object holds f . (b₁ * v) = b₁ * (f . v)
let r be Real; :: thesis: f . (r * v) = r * (f . v)
consider x being Point of V, a being Real such that
B11: ( v = x + (a * x0) & x in X ) by AD2;
r * v = r * (x + (a * x0)) by B11, NORMSP_3:28
.= (r * x) + (r * (a * x0)) by RLVECT_1:def 5
.= (r * x) + ((r * a) * x0) by RLVECT_1:def 7 ;
hence f . (r * v) = r * a by A1, B0, B11, RLSUB_1:21
.= r * (f . v) by A1, B11 ;
:: thesis: verum

end;

hence f is linear-Functional of (NLin M0) by B1; :: thesis: verum

end;

then reconsider f = f as linear-Functional of (NLin M0) ;
A5: for v being Point of (NLin M0) holds |.(f . v).| <= (1 / d) * ||.v.||

proof

let v be Point of (NLin M0); :: thesis: |.(f . v).| <= (1 / d) * ||.v.||
consider x being Point of V, a being Real such that
B5: ( v = x + (a * x0) & x in X ) by AD2;

per cases ( a = 0 or a <> 0 ) ;

suppose a = 0 ; :: thesis: |.(f . v).| <= (1 / d) * ||.v.||

then |.(f . (x + (a * x0))).| = 0 by A1, B5, ABSVALUE:2;
hence |.(f . v).| <= (1 / d) * ||.v.|| by AS2, B5; :: thesis: verum

end;

suppose B6: a <> 0 ; :: thesis: |.(f . v).| <= (1 / d) * ||.v.||

C3: ||.(x + (a * x0)).|| = ||.((1 * x) + (a * x0)).|| by RLVECT_1:def 8
.= ||.(((a * (1 / a)) * x) + (a * x0)).|| by B6, XCMPLX_1:106
.= ||.((a * ((1 / a) * x)) + (a * x0)).|| by RLVECT_1:def 7
.= ||.(a * (((1 / a) * x) + x0)).|| by RLVECT_1:def 5
.= |.a.| * ||.(((1 / a) * x) + x0).|| by NORMSP_1:def 1 ;
C4: ||.(((1 / a) * x) + x0).|| = ||.(- (((1 / a) * x) + x0)).|| by NORMSP_1:2
.= ||.((- ((1 / a) * x)) - x0).|| by RLVECT_1:30 ;
set s = ||.((- ((1 / a) * x)) - x0).||;
C52: - ((1 / a) * x) = (1 / a) * (- x) by RLVECT_1:25;
- x in X by B0, B5, RLSUB_1:22;
then - ((1 / a) * x) in X by B0, C52, RLSUB_1:21;
then ||.((- ((1 / a) * x)) - x0).|| in Z by AS2;
then C5: ||.((- ((1 / a) * x)) - x0).|| >= d by AS2, U2, SEQ_4:def 2;
|.a.| >= 0 by COMPLEX1:46;
then |.a.| * ||.((- ((1 / a) * x)) - x0).|| >= |.a.| * d by C5, XREAL_1:64;
then ||.(x + (a * x0)).|| / d >= |.a.| by AS2, C3, C4, XREAL_1:77;
then (1 / d) * ||.(x + (a * x0)).|| >= |.a.| by XCMPLX_1:99;
then |.(f . (x + (a * x0))).| <= (1 / d) * ||.(x + (a * x0)).|| by A1, B5;
hence |.(f . v).| <= (1 / d) * ||.v.|| by B5, NORMSP_3:28; :: thesis: verum

end;

end;

end;

then f is Lipschitzian by AS2;
then reconsider f = f as Lipschitzian linear-Functional of (NLin M0) ;
reconsider F = f as Point of (DualSp (NLin M0)) by DUALSP01:def 10;
consider g being Lipschitzian linear-Functional of V, G being Point of (DualSp V) such that
C1: ( g = G & g | the carrier of (NLin M0) = f & ||.G.|| = ||.F.|| ) by DUALSP01:36;
A31: for x being Point of V st x in X holds
(Bound2Lipschitz (G,V)) . x = 0

proof

let x be Point of V; :: thesis: ( x in X implies (Bound2Lipschitz (G,V)) . x = 0 )
assume A32: x in X ; :: thesis: (Bound2Lipschitz (G,V)) . x = 0
x = x + (0. V) ;
then A33: x = x + (0 * x0) by RLVECT_1:10;
then A34: x in NLin M0 by X01, A32;
thus (Bound2Lipschitz (G,V)) . x = G . x by SUBSET_1:def 8
.= f . x by A34, C1, FUNCT_1:49
.= 0 by A33, A32, A34, A1 ; :: thesis: verum

end;

A12: (Bound2Lipschitz (G,V)) . x0 = G . x0 by SUBSET_1:def 8
.= f . x0 by C1, V21, FUNCT_1:49
.= 1 by A1, V2, D1, V21 ;
take G ; :: thesis: ( ( for x being Point of V st x in X holds
(Bound2Lipschitz (G,V)) . x = 0 ) & (Bound2Lipschitz (G,V)) . x0 = 1 & ||.G.|| = 1 / d )

now :: thesis: for r being Real st r in PreNorms f holds
r <= 1 / d

let r be Real; :: thesis: ( r in PreNorms f implies r <= 1 / d )
assume r in PreNorms f ; :: thesis: r <= 1 / d
then consider t being VECTOR of (NLin M0) such that
C1: ( r = |.(f . t).| & ||.t.|| <= 1 ) ;
C3: |.(f . t).| <= (1 / d) * ||.t.|| by A5;
(1 / d) * ||.t.|| <= (1 / d) * 1 by AS2, C1, XREAL_1:64;
hence r <= 1 / d by C1, C3, XXREAL_0:2; :: thesis: verum

end;

then upper_bound (PreNorms f) <= 1 / d by SEQ_4:45;
then B3: ||.F.|| <= 1 / d by DUALSP01:24;

now :: thesis: for s being Real st 0 < s holds
1 <= (||.F.|| * d) + (||.F.|| * s)

let s be Real; :: thesis: ( 0 < s implies 1 <= (||.F.|| * d) + (||.F.|| * s) )
assume 0 < s ; :: thesis: 1 <= (||.F.|| * d) + (||.F.|| * s)
then consider r being Real such that
B32: ( r in Z & r < (lower_bound Z) + s ) by U2, SEQ_4:def 2;
consider x being Point of V such that
B34: ( r = ||.(x - x0).|| & x in X ) by B32, AS2;
B35: x - x0 = x + ((- 1) * x0) by RLVECT_1:16;
then x - x0 in M0 by B34;
then reconsider xx0 = x - x0 as Point of (NLin M0) by AD1, NORMSP_3:31;
|.(f . xx0).| = |.(- 1).| by B35, A1, B34
.= |.1.| by COMPLEX1:52
.= 1 by COMPLEX1:43 ;
then B38: 1 <= ||.F.|| * ||.xx0.|| by DUALSP01:26;
||.xx0.|| = r by NORMSP_3:28, B34;
then ||.F.|| * ||.xx0.|| <= ||.F.|| * (d + s) by AS2, B32, XREAL_1:64;
hence 1 <= (||.F.|| * d) + (||.F.|| * s) by B38, XXREAL_0:2; :: thesis: verum

end;

then 1 <= ||.F.|| * d by NORMSP_3:22;
then 1 / d <= (||.F.|| * d) / d by XREAL_1:72, AS2;
then 1 / d <= ||.F.|| by XCMPLX_1:89, AS2;
hence ( ( for x being Point of V st x in X holds
(Bound2Lipschitz (G,V)) . x = 0 ) & (Bound2Lipschitz (G,V)) . x0 = 1 & ||.G.|| = 1 / d ) by A31, A12, C1, B3, XXREAL_0:1; :: thesis: verum