let F be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: for V being VectSp of F
for W being Subspace of V holds
( zeroCoset (V,W) = (0. V) + W & 0. (VectQuot (V,W)) = zeroCoset (V,W) )
let V be VectSp of F; :: thesis: for W being Subspace of V holds
( zeroCoset (V,W) = (0. V) + W & 0. (VectQuot (V,W)) = zeroCoset (V,W) )
let W be Subspace of V; :: thesis: ( zeroCoset (V,W) = (0. V) + W & 0. (VectQuot (V,W)) = zeroCoset (V,W) )
( 0. V = 0. W & 0. W in W ) by VECTSP_4:11;
hence zeroCoset (V,W) = (0. V) + W by VECTSP_4:49; :: thesis: 0. (VectQuot (V,W)) = zeroCoset (V,W)
thus 0. (VectQuot (V,W)) = zeroCoset (V,W) by Def6; :: thesis: verum