theorem LMQ10: :: NORMSP_3:59

for V being RealLinearSpace
for W being Subspace of V
for A being VECTOR of (VectQuot (V,W))
for v being VECTOR of V
for a being Real st A = v + W holds
- A = (- v) + W