theorem :: NORMSP_3:61

for V being RealLinearSpace
for W being Subspace of V
for A1, A2 being VECTOR of (VectQuot (V,W))
for v1, v2 being VECTOR of V st A1 = v1 + W & A2 = v2 + W holds
A1 - A2 = (v1 - v2) + W