theorem Th23: :: VECTSP10:23

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 v being Vector of V holds
( v + W is Coset of W & v + W is Vector of (VectQuot (V,W)) )