:: deftheorem defines zeroCoset NORMSP_3:def 14 :
for V being RealLinearSpace
for W being Subspace of V holds zeroCoset (V,W) = the carrier of W;