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 A being Vector of (VectQuot (V,W))
for v being Vector of V
for a being Scalar of st A = v + W holds
a * A = (a * v) + W