let V be RealNormSpace; :: thesis: for x0 being Point of V st x0 <> 0. V holds
ex F being Point of (DualSp V) st
( ||.F.|| = 1 & (Bound2Lipschitz (F,V)) . x0 = ||.x0.|| )
let x0 be Point of V; :: thesis: ( x0 <> 0. V implies ex F being Point of (DualSp V) st
( ||.F.|| = 1 & (Bound2Lipschitz (F,V)) . x0 = ||.x0.|| ) )
assume AS: x0 <> 0. V ; :: thesis: ex F being Point of (DualSp V) st
( ||.F.|| = 1 & (Bound2Lipschitz (F,V)) . x0 = ||.x0.|| )
then consider G being Point of (DualSp V) such that
A2: ( (Bound2Lipschitz (G,V)) . x0 = 1 & ||.G.|| = 1 / ||.x0.|| ) by Lm65a;
reconsider d = ||.x0.|| as Real ;
reconsider F = d * G as Point of (DualSp V) ;
take F ; :: thesis: ( ||.F.|| = 1 & (Bound2Lipschitz (F,V)) . x0 = ||.x0.|| )
A4: ||.F.|| = |.d.| * ||.G.|| by NORMSP_1:def 1
.= d * (1 / d) by A2, ABSVALUE:def 1
.= 1 by AS, NORMSP_0:def 5, XCMPLX_1:106 ;
(Bound2Lipschitz (F,V)) . x0 = d * (G . x0) by DUALSP01:30, SUBSET_1:def 8
.= d * ((Bound2Lipschitz (G,V)) . x0) by SUBSET_1:def 8 ;
hence ( ||.F.|| = 1 & (Bound2Lipschitz (F,V)) . x0 = ||.x0.|| ) by A2, A4; :: thesis: verum