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

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