let V be RealLinearSpace; :: thesis: for W being Subspace of V holds the carrier of (VectQuot (V,W)) = CosetSet (V,W)
let W be Subspace of V; :: thesis: the carrier of (VectQuot (V,W)) = CosetSet (V,W)
set X = RLSp2RVSp V;
set Y = RLSp2RVSp W;
thus the carrier of (VectQuot (V,W)) = CosetSet ((RLSp2RVSp V),(RLSp2RVSp W)) by VECTSP10:def 6
.= CosetSet (V,W) by LMQ05 ; :: thesis: verum