let V be RealNormSpace; :: thesis: for x being Point of V
for M being non empty Subspace of V st not x in M holds
ex L being non empty real-membered bounded_below set ex U being non empty real-membered bounded_above set st
( L = { ||.(x - m).|| where m is Point of V : m in M } & U = { (x .|. y) where y is Point of (DualSp V) : ( y in Ort_Comp M & ||.y.|| <= 1 ) } & inf L = sup U & sup U in U & ( 0 < inf L implies ex v being Point of (DualSp V) st
( ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L ) ) & ( for m0 being Point of V st m0 in M & ||.(x - m0).|| = inf L holds
for v being Point of (DualSp V) st ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L holds
x - m0,v are_parallel ) )
let x be Point of V; :: thesis: for M being non empty Subspace of V st not x in M holds
ex L being non empty real-membered bounded_below set ex U being non empty real-membered bounded_above set st
( L = { ||.(x - m).|| where m is Point of V : m in M } & U = { (x .|. y) where y is Point of (DualSp V) : ( y in Ort_Comp M & ||.y.|| <= 1 ) } & inf L = sup U & sup U in U & ( 0 < inf L implies ex v being Point of (DualSp V) st
( ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L ) ) & ( for m0 being Point of V st m0 in M & ||.(x - m0).|| = inf L holds
for v being Point of (DualSp V) st ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L holds
x - m0,v are_parallel ) )
let M be non empty Subspace of V; :: thesis: ( not x in M implies ex L being non empty real-membered bounded_below set ex U being non empty real-membered bounded_above set st
( L = { ||.(x - m).|| where m is Point of V : m in M } & U = { (x .|. y) where y is Point of (DualSp V) : ( y in Ort_Comp M & ||.y.|| <= 1 ) } & inf L = sup U & sup U in U & ( 0 < inf L implies ex v being Point of (DualSp V) st
( ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L ) ) & ( for m0 being Point of V st m0 in M & ||.(x - m0).|| = inf L holds
for v being Point of (DualSp V) st ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L holds
x - m0,v are_parallel ) ) )
assume A1: not x in M ; :: thesis: ex L being non empty real-membered bounded_below set ex U being non empty real-membered bounded_above set st
( L = { ||.(x - m).|| where m is Point of V : m in M } & U = { (x .|. y) where y is Point of (DualSp V) : ( y in Ort_Comp M & ||.y.|| <= 1 ) } & inf L = sup U & sup U in U & ( 0 < inf L implies ex v being Point of (DualSp V) st
( ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L ) ) & ( for m0 being Point of V st m0 in M & ||.(x - m0).|| = inf L holds
for v being Point of (DualSp V) st ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L holds
x - m0,v are_parallel ) )
reconsider L = { ||.(x - m).|| where m is Point of V : m in M } as non empty real-membered bounded_below set by Th18;
reconsider U = { (x .|. y) where y is Point of (DualSp V) : ( y in Ort_Comp M & ||.y.|| <= 1 ) } as non empty real-membered bounded_above set by Th19;
take L ; :: thesis: ex U being non empty real-membered bounded_above set st
( L = { ||.(x - m).|| where m is Point of V : m in M } & U = { (x .|. y) where y is Point of (DualSp V) : ( y in Ort_Comp M & ||.y.|| <= 1 ) } & inf L = sup U & sup U in U & ( 0 < inf L implies ex v being Point of (DualSp V) st
( ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L ) ) & ( for m0 being Point of V st m0 in M & ||.(x - m0).|| = inf L holds
for v being Point of (DualSp V) st ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L holds
x - m0,v are_parallel ) )
take U ; :: thesis: ( L = { ||.(x - m).|| where m is Point of V : m in M } & U = { (x .|. y) where y is Point of (DualSp V) : ( y in Ort_Comp M & ||.y.|| <= 1 ) } & inf L = sup U & sup U in U & ( 0 < inf L implies ex v being Point of (DualSp V) st
( ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L ) ) & ( for m0 being Point of V st m0 in M & ||.(x - m0).|| = inf L holds
for v being Point of (DualSp V) st ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L holds
x - m0,v are_parallel ) )
thus L = { ||.(x - m).|| where m is Point of V : m in M } ; :: thesis: ( U = { (x .|. y) where y is Point of (DualSp V) : ( y in Ort_Comp M & ||.y.|| <= 1 ) } & inf L = sup U & sup U in U & ( 0 < inf L implies ex v being Point of (DualSp V) st
( ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L ) ) & ( for m0 being Point of V st m0 in M & ||.(x - m0).|| = inf L holds
for v being Point of (DualSp V) st ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L holds
x - m0,v are_parallel ) )
thus U = { (x .|. y) where y is Point of (DualSp V) : ( y in Ort_Comp M & ||.y.|| <= 1 ) } ; :: thesis: ( inf L = sup U & sup U in U & ( 0 < inf L implies ex v being Point of (DualSp V) st
( ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L ) ) & ( for m0 being Point of V st m0 in M & ||.(x - m0).|| = inf L holds
for v being Point of (DualSp V) st ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L holds
x - m0,v are_parallel ) )
set d = inf L;
A2: inf L = lower_bound L ;

A3: now :: thesis: for e being Real st 0 < e holds
ex me being Point of V st
( ||.(x - me).|| < (inf L) + e & me in M )

let e be Real; :: thesis: ( 0 < e implies ex me being Point of V st
( ||.(x - me).|| < (inf L) + e & me in M ) )
assume 0 < e ; :: thesis: ex me being Point of V st
( ||.(x - me).|| < (inf L) + e & me in M )
then consider r being Real such that
A4: ( r in L & r < (inf L) + e ) by A2, SEQ_4:def 2;
consider me being Point of V such that
A5: ( r = ||.(x - me).|| & me in M ) by A4;
take me = me; :: thesis: ( ||.(x - me).|| < (inf L) + e & me in M )
thus ( ||.(x - me).|| < (inf L) + e & me in M ) by A4, A5; :: thesis: verum

end;

A6: now :: thesis: for y being Point of (DualSp V) st y in Ort_Comp M & ||.y.|| <= 1 holds
x .|. y <= inf L

let y be Point of (DualSp V); :: thesis: ( y in Ort_Comp M & ||.y.|| <= 1 implies x .|. y <= inf L )
assume A7: ( y in Ort_Comp M & ||.y.|| <= 1 ) ; :: thesis: x .|. y <= inf L

A8: now :: thesis: for e0 being Real st 0 < e0 holds
x .|. y < (inf L) + e0

let e0 be Real; :: thesis: ( 0 < e0 implies x .|. y < (inf L) + e0 )
assume A9: 0 < e0 ; :: thesis: x .|. y < (inf L) + e0
set e = e0 / 2;
A10: ( 0 < e0 / 2 & e0 / 2 < e0 ) by A9, XREAL_1:216;
consider me being Point of V such that
A11: ( ||.(x - me).|| < (inf L) + (e0 / 2) & me in M ) by A3, A9;
me .|. y = 0 by A7, A11, Th16;
then A12: x .|. y = (x .|. y) - (me .|. y)
.= (x - me) .|. y by Th13 ;
A13: |.((x - me) .|. y).| <= ||.(x - me).|| * ||.y.|| by Th2;
||.(x - me).|| * ||.y.|| <= ((inf L) + (e0 / 2)) * 1 by XREAL_1:66, A7, A11;
then A14: |.(x .|. y).| <= (inf L) + (e0 / 2) by A12, A13, XXREAL_0:2;
x .|. y <= |.(x .|. y).| by ABSVALUE:4;
then A15: x .|. y <= (inf L) + (e0 / 2) by A14, XXREAL_0:2;
(inf L) + (e0 / 2) < (inf L) + e0 by XREAL_1:8, A10;
hence x .|. y < (inf L) + e0 by A15, XXREAL_0:2; :: thesis: verum

end;

thus x .|. y <= inf L :: thesis: verum

proof

assume inf L < x .|. y ; :: thesis: contradiction
then 0 < (x .|. y) - (inf L) by XREAL_1:50;
then x .|. y < (inf L) + ((x .|. y) - (inf L)) by A8;
hence contradiction ; :: thesis: verum

end;

end;

A16: for r being Real st r in U holds
r <= inf L

proof

let r be Real; :: thesis: ( r in U implies r <= inf L )
assume r in U ; :: thesis: r <= inf L
then consider y being Point of (DualSp V) such that
A17: ( r = x .|. y & y in Ort_Comp M & ||.y.|| <= 1 ) ;
thus r <= inf L by A6, A17; :: thesis: verum

end;

reconsider xM = x + M as Subset of V ;
reconsider LxM = Lin xM as Subspace of V ;
set S = { ((a * x) + m) where a is Real, m is Point of V : m in M } ;
A44P: for z being object holds
( z in { ((a * x) + m) where a is Real, m is Point of V : m in M } iff z in the carrier of LxM )

proof

let z be object ; :: thesis: ( z in { ((a * x) + m) where a is Real, m is Point of V : m in M } iff z in the carrier of LxM )

hereby :: thesis: ( z in the carrier of LxM implies z in { ((a * x) + m) where a is Real, m is Point of V : m in M } )

assume z in { ((a * x) + m) where a is Real, m is Point of V : m in M } ; :: thesis: z in the carrier of LxM
then consider a being Real, m being Point of V such that
A18: ( z = (a * x) + m & m in M ) ;
A19: (x + (2 * m)) - (x + m) = ((x + (2 * m)) - x) - m by RLVECT_1:27
.= (2 * m) - m by RLVECT_4:1
.= (2 * m) - (1 * m) by RLVECT_1:def 8
.= (2 - 1) * m by RLVECT_1:35
.= m by RLVECT_1:def 8 ;
2 * m in M by A18, RLSUB_1:21;
then x + (2 * m) in xM ;
then A20: x + (2 * m) in LxM by RLVECT_3:15;
x + m in xM by A18;
then A21P: x + m in LxM by RLVECT_3:15;

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

suppose a = 0 ; :: thesis: z in the carrier of LxM

then z = (0. V) + m by A18, RLVECT_1:10
.= m ;
hence z in the carrier of LxM by STRUCT_0:def 5, A21P, RLSUB_1:23, A20, A19; :: thesis: verum

end;

suppose A22: a <> 0 ; :: thesis: z in the carrier of LxM

A23: z = (a * x) + (1 * m) by A18, RLVECT_1:def 8
.= (a * x) + ((a * (a ")) * m) by A22, XCMPLX_0:def 7
.= (a * x) + (a * ((a ") * m)) by RLVECT_1:def 7
.= a * (x + ((a ") * m)) by RLVECT_1:def 5 ;
(a ") * m in M by A18, RLSUB_1:21;
then x + ((a ") * m) in xM ;
then z in LxM by A23, RLSUB_1:21, RLVECT_3:15;
hence z in the carrier of LxM by STRUCT_0:def 5; :: thesis: verum

end;

end;

end;

assume z in the carrier of LxM ; :: thesis: z in { ((a * x) + m) where a is Real, m is Point of V : m in M }
then consider l being Linear_Combination of xM such that
A24: z = Sum l by STRUCT_0:def 5, RLVECT_3:14;
consider F being FinSequence of V such that
A25: ( F is one-to-one & rng F = Carrier l & Sum l = Sum (l (#) F) ) by RLVECT_2:def 8;
deffunc H₁( set ) -> Element of REAL = l . (F /. $1);
consider G being FinSequence of REAL such that
A26: len G = len F and
A27: for n being Nat st n in dom G holds
G . n = H₁(n) from FINSEQ_2:sch 1();
A31: for i being Nat st i in dom G holds
G /. i = l . (F /. i)

proof

let i be Nat; :: thesis: ( i in dom G implies G /. i = l . (F /. i) )
assume A32: i in dom G ; :: thesis: G /. i = l . (F /. i)
hence G /. i = G . i by PARTFUN1:def 6
.= l . (F /. i) by A32, A27 ;
:: thesis: verum

end;

A33: rng F c= xM by A25, RLVECT_2:def 6;
A34: for i being Nat st i in dom F holds
F . i in xM

proof

let i be Nat; :: thesis: ( i in dom F implies F . i in xM )
assume i in dom F ; :: thesis: F . i in xM
then F . i in rng F by FUNCT_1:def 3;
hence F . i in xM by A33; :: thesis: verum

end;

deffunc H₂( set ) -> Element of the carrier of V = (G /. $1) * (F /. $1);
consider K being FinSequence of the carrier of V such that
A35: len K = len F and
A36: for n being Nat st n in dom K holds
K . n = H₂(n) from FINSEQ_2:sch 1();
A40: dom K = Seg (len (l (#) F)) by RLVECT_2:def 7, A35, FINSEQ_1:def 3
.= dom (l (#) F) by FINSEQ_1:def 3 ;
A41: dom G = Seg (len (l (#) F)) by RLVECT_2:def 7, FINSEQ_1:def 3, A26
.= dom (l (#) F) by FINSEQ_1:def 3 ;
for i being Nat st i in dom K holds
K . i = (l (#) F) . i

proof

let i be Nat; :: thesis: ( i in dom K implies K . i = (l (#) F) . i )
assume A42: i in dom K ; :: thesis: K . i = (l (#) F) . i
hence K . i = (G /. i) * (F /. i) by A36
.= (l . (F /. i)) * (F /. i) by A31, A40, A42, A41
.= (l (#) F) . i by A42, A40, RLVECT_2:def 7 ;
:: thesis: verum

end;

then K = l (#) F by A40;
hence z in { ((a * x) + m) where a is Real, m is Point of V : m in M } by A34, A35, A36, Th20, A24, A25, A26; :: thesis: verum

end;

reconsider LLxM = RSubNormSpace LxM as SubRealNormSpace of V by Th1;
A45: RLSStruct(# the carrier of LLxM, the ZeroF of LLxM, the addF of LLxM, the Mult of LLxM #) = RLSStruct(# the carrier of LxM, the ZeroF of LxM, the addF of LxM, the Mult of LxM #) by Def1;
then A46: the carrier of LLxM = { ((a * x) + m) where a is Real, m is Point of V : m in M } by A44P, TARSKI:2;
A47: for a1, a2 being Real
for m1, m2 being Point of V st m1 in M & m2 in M & (a1 * x) + m1 = (a2 * x) + m2 holds
( a1 = a2 & m1 = m2 )

proof

let a1, a2 be Real; :: thesis: for m1, m2 being Point of V st m1 in M & m2 in M & (a1 * x) + m1 = (a2 * x) + m2 holds
( a1 = a2 & m1 = m2 )
let m1, m2 be Point of V; :: thesis: ( m1 in M & m2 in M & (a1 * x) + m1 = (a2 * x) + m2 implies ( a1 = a2 & m1 = m2 ) )
assume A48: ( m1 in M & m2 in M & (a1 * x) + m1 = (a2 * x) + m2 ) ; :: thesis: ( a1 = a2 & m1 = m2 )
((a1 * x) + m1) - ((a2 * x) + m2) = (((a1 * x) + m1) - (a2 * x)) - m2 by RLVECT_1:27
.= (((a1 * x) - (a2 * x)) + m1) - m2 by RLVECT_1:def 3
.= (((a1 - a2) * x) + m1) - m2 by RLVECT_1:35 ;
then (0. V) + m2 = ((((a1 - a2) * x) + m1) - m2) + m2 by RLVECT_1:15, A48;
then A49: m2 = (((a1 - a2) * x) + m1) - (m2 - m2) by RLVECT_1:29
.= (((a1 - a2) * x) + m1) - (0. V) by RLVECT_1:15
.= ((a1 - a2) * x) + m1 ;
then m2 - m1 = (a1 - a2) * x by RLVECT_4:1;
then A50: (a1 - a2) * x in M by A48, RLSUB_1:23;
thus a1 = a2 :: thesis: m1 = m2

proof

assume a1 <> a2 ; :: thesis: contradiction
then A51: a1 - a2 <> 0 ;
((a1 - a2) ") * ((a1 - a2) * x) in M by A50, RLSUB_1:21;
then (((a1 - a2) ") * (a1 - a2)) * x in M by RLVECT_1:def 7;
then 1 * x in M by A51, XCMPLX_0:def 7;
hence contradiction by A1, RLVECT_1:def 8; :: thesis: verum

end;

then m2 = (0. V) + m1 by RLVECT_1:10, A49
.= m1 ;
hence m1 = m2 ; :: thesis: verum

end;

defpred S₁[ object , object ] means ex m being Point of V ex a being Real st
( m in M & $1 = (a * x) + m & $2 = a * (inf L) );
A52: for s being Element of the carrier of LLxM ex y being Element of REAL st S₁[s,y]

proof

let s be Element of the carrier of LLxM; :: thesis: ex y being Element of REAL st S₁[s,y]
s in { ((a * x) + m) where a is Real, m is Point of V : m in M } by A45, A44P;
then consider a being Real, m being Point of V such that
A53: ( s = (a * x) + m & m in M ) ;
reconsider b = a * (inf L) as Element of REAL by XREAL_0:def 1;
take b ; :: thesis: S₁[s,b]
thus S₁[s,b] by A53; :: thesis: verum

end;

consider f being Function of the carrier of LLxM,REAL such that
A54: for x being Element of the carrier of LLxM holds S₁[x,f . x] from FUNCT_2:sch 3(A52);
T60: for s, t being Point of LLxM holds f . (s + t) = (f . s) + (f . t)

proof

let s, t be Point of LLxM; :: thesis: f . (s + t) = (f . s) + (f . t)
reconsider s1 = s, t1 = t as Point of LxM by A45;
consider m1 being Point of V, a1 being Real such that
A56: ( m1 in M & s = (a1 * x) + m1 & f . s = a1 * (inf L) ) by A54;
consider m2 being Point of V, a2 being Real such that
A57: ( m2 in M & t = (a2 * x) + m2 & f . t = a2 * (inf L) ) by A54;
consider m3 being Point of V, a3 being Real such that
A58: ( m3 in M & s + t = (a3 * x) + m3 & f . (s + t) = a3 * (inf L) ) by A54;
A59: s + t = s1 + t1 by A45
.= ((a1 * x) + m1) + ((a2 * x) + m2) by A56, A57, RLSUB_1:13
.= (((a1 * x) + m1) + (a2 * x)) + m2 by RLVECT_1:def 3
.= (((a1 * x) + (a2 * x)) + m1) + m2 by RLVECT_1:def 3
.= (((a1 + a2) * x) + m1) + m2 by RLVECT_1:def 6
.= ((a1 + a2) * x) + (m1 + m2) by RLVECT_1:def 3 ;
m1 + m2 in M by A56, A57, RLSUB_1:20;
hence f . (s + t) = (a1 + a2) * (inf L) by A47, A59, A58
.= (f . s) + (f . t) by A56, A57 ;
:: thesis: verum

end;

for s being Point of LLxM
for r being Real holds f . (r * s) = r * (f . s)

proof

let s be Point of LLxM; :: thesis: for r being Real holds f . (r * s) = r * (f . s)
let r be Real; :: thesis: f . (r * s) = r * (f . s)
reconsider s1 = s as Point of LxM by A45;
consider m1 being Point of V, a1 being Real such that
A61: ( m1 in M & s = (a1 * x) + m1 & f . s = a1 * (inf L) ) by A54;
consider m3 being Point of V, a3 being Real such that
A62: ( m3 in M & r * s = (a3 * x) + m3 & f . (r * s) = a3 * (inf L) ) by A54;
A63: r * s = the Mult of LLxM . (r,s) by RLVECT_1:def 1
.= r * s1 by RLVECT_1:def 1, A45
.= r * ((a1 * x) + m1) by A61, RLSUB_1:14
.= (r * (a1 * x)) + (r * m1) by RLVECT_1:def 5
.= ((r * a1) * x) + (r * m1) by RLVECT_1:def 7 ;
r * m1 in M by A61, RLSUB_1:21;
hence f . (r * s) = (r * a1) * (inf L) by A47, A63, A62
.= r * (f . s) by A61 ;
:: thesis: verum

end;

then reconsider f = f as linear-Functional of LLxM by HAHNBAN:def 2, HAHNBAN:def 3, T60;
A64: 0 <= inf L

proof

assume A65: inf L < 0 ; :: thesis: contradiction
then consider r being Real such that
A66: ( r in L & r < (inf L) + ((- (inf L)) / 2) ) by SEQ_4:def 2, A2;
consider m being Point of V such that
A67: ( r = ||.(x - m).|| & m in M ) by A66;
||.(x - m).|| < (inf L) / 2 by A66, A67;
hence contradiction by A65; :: thesis: verum

end;

A68: the normF of LLxM = the normF of V | the carrier of LLxM by DUALSP01:def 16;
A69: for s being VECTOR of LLxM holds |.(f . s).| <= 1 * ||.s.||

proof

let s be VECTOR of LLxM; :: thesis: |.(f . s).| <= 1 * ||.s.||
consider m being Point of V, a being Real such that
A70: ( m in M & s = (a * x) + m & f . s = a * (inf L) ) by A54;
A71: |.(f . s).| = |.a.| * |.(inf L).| by COMPLEX1:65, A70
.= |.a.| * (inf L) by A64, COMPLEX1:43 ;

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

suppose a = 0 ; :: thesis: |.(f . s).| <= 1 * ||.s.||

hence |.(f . s).| <= 1 * ||.s.|| by A70; :: thesis: verum

end;

suppose A72: a <> 0 ; :: thesis: |.(f . s).| <= 1 * ||.s.||

s = (a * x) + (1 * m) by RLVECT_1:def 8, A70
.= (a * x) + ((a * (a ")) * m) by A72, XCMPLX_0:def 7
.= (a * x) + (a * ((a ") * m)) by RLVECT_1:def 7
.= a * (x - (- ((a ") * m))) by RLVECT_1:def 5 ;
then A73: ||.s.|| = ||.(a * (x - (- ((a ") * m)))).|| by A68, FUNCT_1:49
.= |.a.| * ||.(x - (- ((a ") * m))).|| by NORMSP_1:def 1 ;
(a ") * m in M by A70, RLSUB_1:21;
then - ((a ") * m) in M by RLSUB_1:22;
then ||.(x - (- ((a ") * m))).|| in L ;
then A74: inf L <= ||.(x - (- ((a ") * m))).|| by SEQ_4:def 2, A2;
0 <= |.a.| by COMPLEX1:46;
hence |.(f . s).| <= 1 * ||.s.|| by A71, A73, XREAL_1:64, A74; :: thesis: verum

end;

end;

end;

then reconsider f = f as Lipschitzian linear-Functional of LLxM by DUALSP01:def 9;
reconsider pf = f as Point of (DualSp LLxM) by DUALSP01:def 10;

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 LLxM such that
A75: r = |.(f . t).| and
A76: ||.t.|| <= 1 ;
|.(f . t).| <= 1 * ||.t.|| by A69;
hence r <= 1 by A75, A76, XXREAL_0:2; :: thesis: verum

end;

then A78P: upper_bound (PreNorms f) <= 1 by SEQ_4:45;
then A78: ||.pf.|| <= 1 by DUALSP01:24;
consider g being Lipschitzian linear-Functional of V, pg being Point of (DualSp V) such that
A79: ( g = pg & g | the carrier of LLxM = f & ||.pg.|| = ||.pf.|| ) by DUALSP01:36;
A80: ||.pg.|| <= 1 by A78P, A79, DUALSP01:24;
A81: (1 * x) + (0. V) = x by RLVECT_1:def 8;
0. V in M by RLSUB_1:17;
then A82: x in the carrier of LLxM by A46, A81;
A83: x .|. pg = f . x by A79, FUNCT_1:49, A82;
consider m being Point of V, a being Real such that
A84: ( m in M & x = (a * x) + m & f . x = a * (inf L) ) by A54, A82;
A85: (1 * x) + (0. V) = (a * x) + m by A84, RLVECT_1:def 8;
0. V in M by RLSUB_1:17;
then A86P: a = 1 by A47, A84, A85;
for m being VECTOR of V st m in M holds
m,pg are_orthogonal

proof

let m be VECTOR of V; :: thesis: ( m in M implies m,pg are_orthogonal )
assume A87: m in M ; :: thesis: m,pg are_orthogonal
A88: (0 * x) + m = (0. V) + m by RLVECT_1:10
.= m ;
then A89: m in the carrier of LLxM by A46, A87;
consider m1 being Point of V, a being Real such that
A91: ( m1 in M & m = (a * x) + m1 & f . m = a * (inf L) ) by A54, A89;
a = 0 by A87, A88, A91, A47;
hence m,pg are_orthogonal by A91, A79, FUNCT_1:49, A89; :: thesis: verum

end;

then pg in { v where v is VECTOR of (DualSp V) : for w being VECTOR of V st w in M holds
w,v are_orthogonal } ;
then A92P: pg in the carrier of (Ort_Comp M) by Def5;
then A92: pg in Ort_Comp M by STRUCT_0:def 5;
for s being Real st 0 < s holds
ex r being Real st
( r in U & (inf L) - s < r )

proof

let s be Real; :: thesis: ( 0 < s implies ex r being Real st
( r in U & (inf L) - s < r ) )
assume A94: 0 < s ; :: thesis: ex r being Real st
( r in U & (inf L) - s < r )
take inf L ; :: thesis: ( inf L in U & (inf L) - s < inf L )
thus inf L in U by A92, A86P, A80, A83, A84; :: thesis: (inf L) - s < inf L
(inf L) - s < (inf L) - 0 by XREAL_1:15, A94;
hence (inf L) - s < inf L ; :: thesis: verum

end;

then HP1: inf L = upper_bound U by A16, SEQ_4:def 1;
hence inf L = sup U ; :: thesis: ( sup U in U & ( 0 < inf L implies ex v being Point of (DualSp V) st
( ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L ) ) & ( for m0 being Point of V st m0 in M & ||.(x - m0).|| = inf L holds
for v being Point of (DualSp V) st ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L holds
x - m0,v are_parallel ) )
thus sup U in U by A92, A86P, A80, A83, A84, HP1; :: thesis: ( ( 0 < inf L implies ex v being Point of (DualSp V) st
( ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L ) ) & ( for m0 being Point of V st m0 in M & ||.(x - m0).|| = inf L holds
for v being Point of (DualSp V) st ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L holds
x - m0,v are_parallel ) )
thus ( 0 < inf L implies ex pg being Point of (DualSp V) st
( ||.pg.|| = 1 & pg in Ort_Comp M & x .|. pg = inf L ) ) :: thesis: for m0 being Point of V st m0 in M & ||.(x - m0).|| = inf L holds
for v being Point of (DualSp V) st ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L holds
x - m0,v are_parallel

proof

assume A95P: 0 < inf L ; :: thesis: ex pg being Point of (DualSp V) st
( ||.pg.|| = 1 & pg in Ort_Comp M & x .|. pg = inf L )

now :: thesis: for e being Real st 0 < e holds
(((inf L) + e) ") * (inf L) <= ||.pf.||

let e be Real; :: thesis: ( 0 < e implies (((inf L) + e) ") * (inf L) <= ||.pf.|| )
assume 0 < e ; :: thesis: (((inf L) + e) ") * (inf L) <= ||.pf.||
then consider m being Point of V such that
A96: ( ||.(x - m).|| < (inf L) + e & m in M ) by A3;
A97: x - m = (1 * x) - m by RLVECT_1:def 8;
- m in M by RLSUB_1:22, A96;
then x - m in the carrier of LLxM by A97, A46;
then reconsider xm = x - m as Point of LLxM ;
consider m1 being Point of V, a being Real such that
A98: ( m1 in M & xm = (a * x) + m1 & f . xm = a * (inf L) ) by A54;
- m in M by A96, RLSUB_1:22;
then A100P: f . xm = 1 * (inf L) by A97, A98, A47
.= inf L ;
x - m <> 0. V by RLVECT_1:21, A1, A96;
then A101P: ||.(x - m).|| <> 0 by NORMSP_0:def 5;
then A101: ||.xm.|| <> 0 by A68, FUNCT_1:49;
set s = (||.xm.|| ") * xm;
A102: ||.((||.xm.|| ") * xm).|| = |.(||.xm.|| ").| * ||.xm.|| by NORMSP_1:def 1
.= 1 by XCMPLX_0:def 7, A101 ;
A103: |.(f . ((||.xm.|| ") * xm)).| = |.((||.xm.|| ") * (f . xm)).| by HAHNBAN:def 3
.= (||.xm.|| ") * (inf L) by A100P, A64, COMPLEX1:43 ;
A104: ||.xm.|| < (inf L) + e by A96, A68, FUNCT_1:49;
0 < ||.xm.|| by A101P, A68, FUNCT_1:49;
then ((inf L) + e) " < ||.xm.|| " by A104, XREAL_1:88;
then A106: (((inf L) + e) ") * (inf L) <= |.(f . ((||.xm.|| ") * xm)).| by A103, XREAL_1:64, A64;
|.(f . ((||.xm.|| ") * xm)).| in PreNorms f by A102;
then |.(f . ((||.xm.|| ") * xm)).| <= upper_bound (PreNorms f) by SEQ_4:def 1;
then (((inf L) + e) ") * (inf L) <= upper_bound (PreNorms f) by A106, XXREAL_0:2;
hence (((inf L) + e) ") * (inf L) <= ||.pf.|| by DUALSP01:24; :: thesis: verum

end;

then 1 <= ||.pf.|| by Lm1, A95P;
then ||.pf.|| = 1 by A78, XXREAL_0:1;
hence ex pg being Point of (DualSp V) st
( ||.pg.|| = 1 & pg in Ort_Comp M & x .|. pg = inf L ) by A79, A86P, A92P, A83, A84, STRUCT_0:def 5; :: thesis: verum

end;

now :: thesis: for m0 being Point of V st m0 in M & ||.(x - m0).|| = inf L holds
for pg being Point of (DualSp V) st ||.pg.|| = 1 & pg in Ort_Comp M & x .|. pg = inf L holds
x - m0,pg are_parallel

let m0 be Point of V; :: thesis: ( m0 in M & ||.(x - m0).|| = inf L implies for pg being Point of (DualSp V) st ||.pg.|| = 1 & pg in Ort_Comp M & x .|. pg = inf L holds
x - m0,pg are_parallel )
assume A107: ( m0 in M & ||.(x - m0).|| = inf L ) ; :: thesis: for pg being Point of (DualSp V) st ||.pg.|| = 1 & pg in Ort_Comp M & x .|. pg = inf L holds
x - m0,pg are_parallel
let pg be Point of (DualSp V); :: thesis: ( ||.pg.|| = 1 & pg in Ort_Comp M & x .|. pg = inf L implies x - m0,pg are_parallel )
assume A108: ( ||.pg.|| = 1 & pg in Ort_Comp M & x .|. pg = inf L ) ; :: thesis: x - m0,pg are_parallel
(x - m0) .|. pg = (inf L) - (m0 .|. pg) by A108, Th13
.= (inf L) - 0 by A107, Th16, A108
.= ||.(x - m0).|| * ||.pg.|| by A107, A108 ;
hence x - m0,pg are_parallel ; :: thesis: verum

end;

hence for m0 being Point of V st m0 in M & ||.(x - m0).|| = inf L holds
for v being Point of (DualSp V) st ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L holds
x - m0,v are_parallel ; :: thesis: verum