theorem LMQ13: :: NORMSP_3:62

for V being RealLinearSpace
for W being Subspace of V holds
( 0. (VectQuot (V,W)) = the carrier of W & 0. (VectQuot (V,W)) = (0. V) + W )