let X be RealUnitarySpace; :: thesis: for f being linear-Functional of X st ( for x being VECTOR of X holds f . x = 0 ) holds
f is Lipschitzian
let f be linear-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
for x being VECTOR of X holds |.(f . x).| <= 1 * ||.x.||

proof

let x be VECTOR of X; :: thesis: |.(f . x).| <= 1 * ||.x.||
0 <= ||.x.|| by BHSP_1:28;
hence |.(f . x).| <= 1 * ||.x.|| by A1, COMPLEX1:44; :: thesis: verum

end;

hence f is Lipschitzian by BHSP_6:def 4; :: thesis: verum