let X be RealNormSpace; :: thesis: for f being Lipschitzian linear-Functional of X holds Bound2Lipschitz (f,X) = f

let f be Lipschitzian linear-Functional of X; :: thesis: Bound2Lipschitz (f,X) = f

f in BoundedLinearFunctionals X by Def9;

hence Bound2Lipschitz (f,X) = f by SUBSET_1:def 8; :: thesis: verum

let f be Lipschitzian linear-Functional of X; :: thesis: Bound2Lipschitz (f,X) = f

f in BoundedLinearFunctionals X by Def9;

hence Bound2Lipschitz (f,X) = f by SUBSET_1:def 8; :: thesis: verum