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

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