let V be RealLinearSpace; :: thesis: for W being Subspace of V holds
( 0. (VectQuot (V,W)) = the carrier of W & 0. (VectQuot (V,W)) = (0. V) + W )
let W be Subspace of V; :: thesis: ( 0. (VectQuot (V,W)) = the carrier of W & 0. (VectQuot (V,W)) = (0. V) + W )
thus 0. (VectQuot (V,W)) = zeroCoset (V,W) by LMQ08
.= the carrier of W ; :: thesis: 0. (VectQuot (V,W)) = (0. V) + W
hence 0. (VectQuot (V,W)) = (0. V) + W by RLSUB_1:44; :: thesis: verum