theorem Th22: :: VECTSP10:22

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