let X be RealBanachSpace; :: thesis:
let M be non empty Subset of X; :: thesis:
assume that
A2: X is Reflexive and
A3: M is linearly-closed and
A4: M is closed ; :: thesis:
set M0 = NLin M;
X1: the carrier of (NLin M) = M by NORMSP_3:31, A3;
X2: the carrier of (NLin M) c= the carrier of X by DUALSP01:def 16;
for y being Point of (DualSp (DualSp (NLin M))) ex x being Point of (NLin M) st
for g being Point of (DualSp (NLin M)) holds y . g = g . x

let y be Point of (DualSp (DualSp (NLin M))); :: thesis:
reconsider y1 = y as Lipschitzian linear-Functional of (DualSp (NLin M)) by DUALSP01:def 10;
defpred S₁[ Function, Function] means $2 = $1 | M;
P0: for x being Element of (DualSp X) ex y being Element of (DualSp (NLin M)) st S₁[x,y]

let x be Element of (DualSp X); :: thesis:
reconsider x0 = x as Lipschitzian linear-Functional of X by DUALSP01:def 10;
reconsider y0 = x0 | M as Function of (NLin M),REAL by X1, FUNCT_2:32;
B1: y0 is additive

proof

let s, t be Point of (NLin M); :: according to HAHNBAN:def 2 :: thesis:
reconsider s1 = s, t1 = t as Point of X by X2;
C1: s + t = s1 + t1 by NORMSP_3:28;
thus y0 . (s + t) = x0 . (s + t) by X1, FUNCT_1:49
.= (x0 . s1) + (x0 . t1) by C1, HAHNBAN:def 2
.= ((x0 | M) . s) + (x0 . t) by X1, FUNCT_1:49
.= (y0 . s) + (y0 . t) by X1, FUNCT_1:49 ; :: thesis:

end;

B2: y0 is homogeneous

proof

let s be Point of (NLin M); :: according to HAHNBAN:def 3 :: thesis:
let r be Real; :: thesis:
reconsider s1 = s as Point of X by X2;
C2: r * s = r * s1 by NORMSP_3:28;
thus y0 . (r * s) = x0 . (r * s) by X1, FUNCT_1:49
.= r * (x0 . s) by C2, HAHNBAN:def 3
.= r * (y0 . s) by X1, FUNCT_1:49 ; :: thesis:

end;

for s being Point of (NLin M) holds |.(y0 . s).| <= ||.x.|| * ||.s.||

proof

let s be Point of (NLin M); :: thesis:
reconsider s1 = s as Point of X by X2;
C3: ||.s.|| = ||.s1.|| by NORMSP_3:28;
|.(y0 . s).| = |.(x0 . s).| by X1, FUNCT_1:49;
hence |.(y0 . s).| <= ||.x.|| * ||.s.|| by C3, DUALSP01:26; :: thesis:

end;

then y0 is Lipschitzian ;
then reconsider y = y0 as Element of (DualSp (NLin M)) by B1, B2, DUALSP01:def 10;
take y ; :: thesis:
thus y = x | M ; :: thesis:

end;

consider T being Function of (DualSp X),(DualSp (NLin M)) such that
P11: for x being Element of (DualSp X) holds S₁[x,T . x] from FUNCT_2:sch 3(P0);
D1: T is additive

proof

let f, g be Point of (DualSp X); :: according to VECTSP_1:def 19 :: thesis:
E1: ( T . (f + g) is Function of (NLin M),REAL & (T . f) + (T . g) is Function of (NLin M),REAL ) by DUALSP01:def 10;
for x being Point of (NLin M) holds (T . (f + g)) . x = ((T . f) + (T . g)) . x

proof

let x be Point of (NLin M); :: thesis:
reconsider x1 = x as Point of X by X2;
( T . f = f | M & T . g = g | M ) by P11;
then reconsider fm = f | M, gm = g | M as Point of (DualSp (NLin M)) ;
F2: ( fm . x = f . x & gm . x = g . x ) by X1, FUNCT_1:49;
thus (T . (f + g)) . x = ((f + g) | M) . x by P11
.= (f + g) . x by X1, FUNCT_1:49
.= (f . x1) + (g . x1) by DUALSP01:29
.= ((T . f) . x) + (gm . x) by P11, F2
.= ((T . f) . x) + ((T . g) . x) by P11
.= ((T . f) + (T . g)) . x by DUALSP01:29 ; :: thesis:

end;

hence T . (f + g) = (T . f) + (T . g) by E1, FUNCT_2:def 8; :: thesis:

end;

T is homogeneous

proof

let f be Point of (DualSp X); :: according to LOPBAN_1:def 5 :: thesis:
let r be Real; :: thesis:
E3: ( T . (r * f) is Function of (NLin M),REAL & r * (T . f) is Function of (NLin M),REAL ) by DUALSP01:def 10;
for x being Point of (NLin M) holds (T . (r * f)) . x = (r * (T . f)) . x

proof

let x be Point of (NLin M); :: thesis:
reconsider x1 = x as Point of X by X2;
T . f = f | M by P11;
then reconsider fm = f | M as Point of (DualSp (NLin M)) ;
F4: fm . x = f . x by X1, FUNCT_1:49;
thus (T . (r * f)) . x = ((r * f) | M) . x by P11
.= (r * f) . x by X1, FUNCT_1:49
.= r * (f . x1) by DUALSP01:30
.= r * ((T . f) . x) by P11, F4
.= (r * (T . f)) . x by DUALSP01:30 ; :: thesis:

end;

hence T . (r * f) = r * (T . f) by E3, FUNCT_2:def 8; :: thesis:

end;

then reconsider T = T as LinearOperator of (DualSp X),(DualSp (NLin M)) by D1;
for v being Point of (DualSp X) holds ||.(T . v).|| <= 1 * ||.v.||

proof

let v be Point of (DualSp X); :: thesis:
reconsider v1 = v as Lipschitzian linear-Functional of X by DUALSP01:def 10;
B0: T . v = v | M by P11;
then reconsider vm = v | M as Point of (DualSp (NLin M)) ;
reconsider vm1 = vm as Lipschitzian linear-Functional of (NLin M) by DUALSP01:def 10;

now :: thesis:

let r be Real; :: thesis:
assume r in PreNorms vm1 ; :: thesis:
then consider t being VECTOR of (NLin M) such that
B1: ( r = |.(vm1 . t).| & ||.t.|| <= 1 ) ;
reconsider t1 = t as Point of X by X2;
B2: |.(vm . t).| = |.(v . t1).| by X1, FUNCT_1:49;
||.t1.|| = ||.t.|| by NORMSP_3:28;
hence r in PreNorms v1 by B1, B2; :: thesis:

end;

then PreNorms vm1 c= PreNorms v1 ;
then upper_bound (PreNorms vm1) <= upper_bound (PreNorms v1) by SEQ_4:48;
then ||.vm.|| <= upper_bound (PreNorms v1) by DUALSP01:24;
hence ||.(T . v).|| <= 1 * ||.v.|| by B0, DUALSP01:24; :: thesis:

end;

then reconsider T = T as Lipschitzian LinearOperator of (DualSp X),(DualSp (NLin M)) by LOPBAN_1:def 8;
P2: for f being Point of (DualSp X)
for x being Point of X st x in M holds
(T . f) . x = f . x

proof

let f be Point of (DualSp X); :: thesis:
let x be Point of X; :: thesis:
assume x in M ; :: thesis:
then (f | M) . x = f . x by FUNCT_1:49;
hence (T . f) . x = f . x by P11; :: thesis:

end;

deffunc H₁( Element of (DualSp X)) -> Element of REAL = y . (T . $1);
consider z being Function of the carrier of (DualSp X),REAL such that
Q10: for f being Element of the carrier of (DualSp X) holds z . f = H₁(f) from FUNCT_2:sch 4();
Q11: z is additive

proof

let s, t be Point of (DualSp X); :: according to HAHNBAN:def 2 :: thesis:
thus z . (s + t) = y . (T . (s + t)) by Q10
.= y . ((T . s) + (T . t)) by VECTSP_1:def 20
.= (y1 . (T . s)) + (y1 . (T . t)) by HAHNBAN:def 2
.= (z . s) + (y . (T . t)) by Q10
.= (z . s) + (z . t) by Q10 ; :: thesis:

end;

Q12: z is homogeneous

proof

let s be Point of (DualSp X); :: according to HAHNBAN:def 3 :: thesis:
let r be Real; :: thesis:
thus z . (r * s) = y . (T . (r * s)) by Q10
.= y . (r * (T . s)) by LOPBAN_1:def 5
.= r * (y1 . (T . s)) by HAHNBAN:def 3
.= r * (z . s) by Q10 ; :: thesis:

end;

proof

let s be Point of (DualSp X); :: thesis:
B1: |.(z . s).| = |.(y . (T . s)).| by Q10;
B2: |.(y1 . (T . s)).| <= ||.y.|| * ||.(T . s).|| by DUALSP01:26;
||.y.|| * ||.(T . s).|| <= ||.y.|| * (||.T1.|| * ||.s.||) by XREAL_1:64, LOPBAN_1:32;
hence |.(z . s).| <= (||.y.|| * ||.T1.||) * ||.s.|| by B1, B2, XXREAL_0:2; :: thesis:

end;

then z is Lipschitzian ;
then reconsider z = z as Point of (DualSp (DualSp X)) by Q11, Q12, DUALSP01:def 10;
consider x being Point of X such that
Q2: for f being Point of (DualSp X) holds z . f = f . x by A2, REFF1;
Q3: for f being Point of (DualSp X) holds y . (T . f) = f . x

proof

let f be Point of (DualSp X); :: thesis:
thus y . (T . f) = z . f by Q10
.= f . x by Q2 ; :: thesis:

end;

AX: x in the carrier of (NLin M)

proof

assume not x in the carrier of (NLin M) ; :: thesis:
then consider f being Point of (DualSp X) such that
B1: for x being Point of X st x in M holds
(Bound2Lipschitz (f,X)) . x = 0 and
B2: (Bound2Lipschitz (f,X)) . x = 1 by A3, A4, X1, Lm64;
reconsider f1 = f as Lipschitzian linear-Functional of X by DUALSP01:def 10;
B3: f1 = Bound2Lipschitz (f,X) by DUALSP01:23;
B4: for x being Point of X st x in M holds
(T . f) . x = 0

proof

let x be Point of X; :: thesis:
assume C1: x in M ; :: thesis:
then f . x = 0 by B1, B3;
hence (T . f) . x = 0 by C1, P2; :: thesis:

end;

B8: T . f is Function of (NLin M),REAL by DUALSP01:def 10;
for x being Point of (NLin M) holds (T . f) . x = (M --> 0) . x

proof

let x be Point of (NLin M); :: thesis:
x in M by X1;
then reconsider x1 = x as Point of X ;
(T . f) . x1 = 0 by X1, B4;
hence (T . f) . x = (M --> 0) . x by X1, FUNCOP_1:7; :: thesis:

end;

then B9: T . f = M --> 0 by X1, B8, FUNCT_2:def 8
.= 0. (DualSp (NLin M)) by X1, DUALSP01:25 ;
f . x = y1 . (0. (DualSp (NLin M))) by B9, Q3
.= 0 by HAHNBAN:20 ;
hence contradiction by B2, B3; :: thesis:

end;

Q4: for f being Point of (DualSp X) holds y . (T . f) = (T . f) . x

proof

let f be Point of (DualSp X); :: thesis:
y . (T . f) = f . x by Q3;
hence y . (T . f) = (T . f) . x by P2, X1, AX; :: thesis:

end;

Q5: for f being Point of (DualSp X) holds y . (f | M) = (f | M) . x

proof

let f be Point of (DualSp X); :: thesis:
T . f = f | M by P11;
hence y . (f | M) = (f | M) . x by Q4; :: thesis:

end;

for g being Point of (DualSp (NLin M)) holds y . g = g . x

proof

let g be Point of (DualSp (NLin M)); :: thesis:
reconsider g1 = g as Lipschitzian linear-Functional of (NLin M) by DUALSP01:def 10;
ex f1 being Lipschitzian linear-Functional of X ex f being Point of (DualSp X) st
( f1 = f & f1 | the carrier of (NLin M) = g1 & ||.f.|| = ||.g.|| ) by DUALSP01:36;
hence y . g = g . x by X1, Q5; :: thesis:

end;

hence ex x being Point of (NLin M) st
for g being Point of (DualSp (NLin M)) holds y . g = g . x by AX; :: thesis:

end;

hence NLin M is Reflexive by REFF1; :: thesis: