:: deftheorem Def6 defines VectQuot VECTSP10:def 6 :
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 b₄ being non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over K holds
( b₄ = VectQuot (V,W) iff ( the carrier of b₄ = CosetSet (V,W) & the addF of b₄ = addCoset (V,W) & 0. b₄ = zeroCoset (V,W) & the lmult of b₄ = lmultCoset (V,W) ) );