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

( 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