theorem LMQ11: :: NORMSP_3:60

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