let X be RealUnitarySpace; :: thesis: for F being linear-Functional of X st F = the carrier of X --> 0 holds
F is Lipschitzian
let F be linear-Functional of X; :: thesis: ( F = the carrier of X --> 0 implies F is Lipschitzian )
assume F = the carrier of X --> 0 ; :: thesis: F is Lipschitzian
then for x being VECTOR of X holds F . x = 0 ;
hence F is Lipschitzian by Th16; :: thesis: verum