let X be RealNormSpace; :: 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 ;
f in BoundedLinearFunctionals X by Def9;
hence (BoundedLinearFunctionalsNorm X) . f = upper_bound (PreNorms (Bound2Lipschitz (f9,X))) by Def13
.= upper_bound (PreNorms f) by Th29 ;
:: thesis: verum