theorem Th21: :: DUALSP01:16
for X being RealNormSpace
for f being Functional of X st ( for x being VECTOR of X holds f . x = 0 ) holds
f is Lipschitzian