for V being RealNormSpace
for x being Point of V st ( for f being Lipschitzian linear-Functional of V holds f . x = 0 ) holds
x = 0. V