theorem Th29: :: DUALSP01:23

for X being RealNormSpace
for f being Lipschitzian linear-Functional of X holds Bound2Lipschitz (f,X) = f