for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for V being VectSp of K
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