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 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 & ||.G.|| = ||.F.|| )