let X be RealUnitarySpace; :: 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 Def10;

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 Def10;

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