let X be RealUnitarySpace; :: thesis: for f being Lipschitzian linear-Functional of X holds (BoundedLinearFunctionalsNorm X) . f = upper_bound (PreNorms f)
let f be Lipschitzian linear-Functional of X; :: thesis: (BoundedLinearFunctionalsNorm X) . f = upper_bound (PreNorms f)
reconsider f9 = f as set ;
thus (BoundedLinearFunctionalsNorm X) . f = upper_bound (PreNorms (Bound2Lipschitz (f9,X))) by Def14
.= upper_bound (PreNorms f) ; :: thesis: verum