let V be RealNormSpace; :: thesis:
let x be Point of (DualSp V); :: thesis:
let M be non empty Subspace of V; :: thesis:
let SM be SubRealNormSpace of V; :: thesis:
assume A1: SM = RSubNormSpace M ; :: thesis:
reconsider L = { ||.(x - m).|| where m is Point of (DualSp V) : m in Ort_Comp M } as non empty real-membered bounded_below set by Th23;
reconsider U = { (y .|. x) where y is Point of V : ( y in M & ||.y.|| <= 1 ) } as non empty real-membered bounded_above set by Th24;
take L ; :: thesis:
take U ; :: thesis:
thus ( L = { ||.(x - m).|| where m is Point of (DualSp V) : m in Ort_Comp M } & U = { (y .|. x) where y is Point of V : ( y in M & ||.y.|| <= 1 ) } ) ; :: thesis:
A2: ( RLSStruct(# the carrier of SM, the ZeroF of SM, the addF of SM, the Mult of SM #) = RLSStruct(# the carrier of M, the ZeroF of M, the addF of M, the Mult of M #) & the normF of SM = the normF of V | the carrier of SM ) by Def1, A1;
reconsider fx = x as Lipschitzian linear-Functional of V by DUALSP01:def 10;
set fxM = fx | the carrier of SM;
dom fx = the carrier of V by FUNCT_2:def 1;
then the carrier of SM c= dom fx by RLSUB_1:def 2, A2;
then ( dom (fx | the carrier of SM) = the carrier of SM & rng (fx | the carrier of SM) c= REAL ) by RELAT_1:62;
then reconsider fxM = fx | the carrier of SM as Function of the carrier of SM,REAL by FUNCT_2:2;
A6P: for s, t being Point of SM holds fxM . (s + t) = (fxM . s) + (fxM . t)

let s, t be Point of SM; :: thesis:
reconsider s1 = s, t1 = t as Point of M by A2;
reconsider s2 = s1, t2 = t1 as Point of V by RLSUB_1:10;
A5P: ( fxM . s = fx . s1 & fxM . t = fx . t1 ) by FUNCT_1:49;
thus fxM . (s + t) = fx . (s1 + t1) by FUNCT_1:49, A2
.= fx . (s2 + t2) by RLSUB_1:13
.= (fxM . s) + (fxM . t) by A5P, HAHNBAN:def 2 ; :: thesis:

end;

for s being Point of SM
for r being Real holds fxM . (r * s) = r * (fxM . s)

let s be Point of SM; :: thesis:
let r be Real; :: thesis:
reconsider s1 = s as Point of M by A2;
reconsider s2 = s1 as Point of V by RLSUB_1:10;
A7: r * s2 = r * s1 by RLSUB_1:14;
A8: r * s = the Mult of SM . (r,s) by RLVECT_1:def 1
.= r * s1 by RLVECT_1:def 1, A2 ;
thus fxM . (r * s) = fx . (r * s2) by A7, A8, FUNCT_1:49
.= r * (fx . s2) by HAHNBAN:def 3
.= r * (fxM . s) by FUNCT_1:49 ; :: thesis:

end;

end;

then reconsider fxM = fxM as Lipschitzian linear-Functional of SM by DUALSP01:def 9;
reconsider xM = fxM as Point of (DualSp SM) by DUALSP01:def 10;

let r be object ; :: according to TARSKI:def 3 :: thesis:
assume r in PreNorms fxM ; :: thesis:
then consider t being VECTOR of SM such that
A17: ( r = |.(fxM . t).| & ||.t.|| <= 1 ) ;
reconsider t1 = t as Point of V by A2, RLSUB_1:10;
t1 in M by STRUCT_0:def 5, A2;
then A19: t1 .|. m = 0 by A16, Th16;
A20: fxm . t1 = t1 .|. (x - m)
.= (t1 .|. x) - (t1 .|. m) by Th12
.= fxM . t by FUNCT_1:49, A19 ;
||.t.|| = ||.t1.|| by A2, FUNCT_1:49;
hence r in PreNorms fxm by A17, A20; :: thesis:

end;

end;

consider fy being Lipschitzian linear-Functional of V, y being Point of (DualSp V) such that
A23: ( fy = y & fy | the carrier of SM = fxM & ||.y.|| = ||.xM.|| ) by DUALSP01:36;
set m0 = x - y;
reconsider fm0 = x - y as Lipschitzian linear-Functional of V by DUALSP01:def 10;
for t being Point of V st t in M holds
t,x - y are_orthogonal

let t be Point of V; :: thesis:
assume A27P: t in M ; :: thesis:
t .|. (x - y) = (t .|. x) - (t .|. y) by Th12
.= (fx . t) - (fxM . t) by A23, A27P, FUNCT_1:49, STRUCT_0:def 5, A2
.= (fx . t) - (fx . t) by A27P, FUNCT_1:49, STRUCT_0:def 5, A2
.= 0 ;
hence t,x - y are_orthogonal ; :: thesis:

end;

then x - y 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 x - y in the carrier of (Ort_Comp M) by Def5;
then A29: x - y in Ort_Comp M by STRUCT_0:def 5;
A30P: x - (x - y) = y by RLVECT_4:1;
A32: for r being Real st r in L holds
||.xM.|| <= r

let r be Real; :: thesis:
assume r in L ; :: thesis:
then consider m being Point of (DualSp V) such that
A33: ( r = ||.(x - m).|| & m in Ort_Comp M ) ;
thus ||.xM.|| <= r by A15, A33; :: thesis:

end;

for s being Real st 0 < s holds
ex r being Real st
( r in L & r < ||.xM.|| + s )

end;

then A35P: ||.xM.|| = lower_bound L by A32, SEQ_4:def 2;
take x - y ; :: thesis:
take fx ; :: thesis:
take xM ; :: thesis:
thus ( x = fx & xM = fx | the carrier of SM & x - y in Ort_Comp M & ||.(x - (x - y)).|| = inf L & inf L in L & ||.(x - (x - y)).|| = ||.xM.|| ) by A29, A30P, A35P, A23; :: thesis:
let y be Point of V; :: thesis:
assume A37: ( ||.y.|| = 1 & y in M & fx . y = ||.(x - (x - y)).|| ) ; :: thesis:
y .|. (x - (x - y)) = (y .|. x) - (y .|. (x - y)) by Th12
.= ||.(x - (x - y)).|| - 0 by A29, A37, Th16
.= ||.(x - (x - y)).|| * ||.y.|| by A37 ;
hence y,x - (x - y) are_parallel ; :: thesis: