theorem SUBTH0: :: NORMSP_3:28

for V being RealNormSpace
for V1 being SubRealNormSpace of V
for x, y being Point of V
for x1, y1 being Point of V1
for a being Real st x = x1 & y = y1 holds
( ||.x.|| = ||.x1.|| & x + y = x1 + y1 & a * x = a * x1 )