let X be RealNormSpace; :: thesis: for f being Functional of X st ( for x being VECTOR of X holds f . x = 0 ) holds
f is Lipschitzian
let f be Functional of X; :: thesis: ( ( for x being VECTOR of X holds f . x = 0 ) implies f is Lipschitzian )
assume A1: for x being VECTOR of X holds f . x = 0 ; :: thesis: f is Lipschitzian
take 0 ; :: according to DUALSP01:def 9 :: thesis: ( 0 <= 0 & ( for x being VECTOR of X holds |.(f . x).| <= 0 * ||.x.|| ) )
thus ( 0 <= 0 & ( for x being VECTOR of X holds |.(f . x).| <= 0 * ||.x.|| ) ) by A1, COMPLEX1:44; :: thesis: verum