theorem Th21: :: VECTSP10:21

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 holds
( zeroCoset (V,W) = (0. V) + W & 0. (VectQuot (V,W)) = zeroCoset (V,W) )