let F be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive 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 STRUCT_0:def 5, VECTSP_4:19;
hence zeroCoset V,W = (0. V) + W by VECTSP_4:64; :: thesis: 0. (VectQuot V,W) = zeroCoset V,W
thus 0. (VectQuot V,W) = zeroCoset V,W by Def6; :: thesis: verum