theorem LMQ08: :: NORMSP_3:57

for V being RealLinearSpace
for W being Subspace of V holds 0. (VectQuot (V,W)) = zeroCoset (V,W)