:: deftheorem defines zeroCoset VECTSP10:def 4 :
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) = the carrier of W;