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

( 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