theorem :: DUALSP01:37

for V being RealNormSpace
for X being SubRealNormSpace of V
for f being Lipschitzian linear-Functional of X
for F being Point of (DualSp X) st f = F & ( for x being VECTOR of X
for v being VECTOR of V st x = v holds
f . x <= ||.v.|| ) holds
ex g being Lipschitzian linear-Functional of V ex G being Point of (DualSp V) st
( g = G & g | the carrier of X = f & ( for x being VECTOR of V holds
( g . x <= ||.x.|| & ||.G.|| = ||.F.|| ) ) )