let X be RealNormSpace; :: thesis: for F being Functional of X st F = the carrier of X --> 0 holds
( F is linear-Functional of X & F is Lipschitzian )
let F be Functional of X; :: thesis: ( F = the carrier of X --> 0 implies ( F is linear-Functional of X & F is Lipschitzian ) )
assume A1: F = the carrier of X --> 0 ; :: thesis: ( F is linear-Functional of X & F is Lipschitzian )
then reconsider F = F as linear-Functional of X by Th23;
for x being VECTOR of X holds F . x = 0 by A1;
hence ( F is linear-Functional of X & F is Lipschitzian ) by Th21; :: thesis: verum