for V being RealNormSpace
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.|| )