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