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

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