let V be RealNormSpace; :: thesis: for x being Point of V st ( for f being Lipschitzian linear-Functional of V holds f . x = 0 ) holds
x = 0. V
let x be Point of V; :: thesis: ( ( for f being Lipschitzian linear-Functional of V holds f . x = 0 ) implies x = 0. V )
assume AS: for f being Lipschitzian linear-Functional of V holds f . x = 0 ; :: thesis: x = 0. V
assume x <> 0. V ; :: thesis: contradiction
then ex G being Point of (DualSp V) st
( (Bound2Lipschitz (G,V)) . x = 1 & ||.G.|| = 1 / ||.x.|| ) by Lm65a;
hence contradiction by AS; :: thesis: verum