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

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