theorem :: NORMSP_4:22

for X being RealNormSpace
for Y being SubRealNormSpace of X
for L being Lipschitzian linear-Functional of X holds L | the carrier of Y is Lipschitzian linear-Functional of Y