let K be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: for V being VectSp of K
for W being Subspace of V
for w being Vector of (VectQuot (V,W)) holds
( w is Coset of W & ex v being Vector of V st w = v + W )
let V be VectSp of K; :: thesis: for W being Subspace of V
for w being Vector of (VectQuot (V,W)) holds
( w is Coset of W & ex v being Vector of V st w = v + W )
let W be Subspace of V; :: thesis: for w being Vector of (VectQuot (V,W)) holds
( w is Coset of W & ex v being Vector of V st w = v + W )
let w be Vector of (VectQuot (V,W)); :: thesis: ( w is Coset of W & ex v being Vector of V st w = v + W )
set qv = VectQuot (V,W);
set cs = CosetSet (V,W);
CosetSet (V,W) = the carrier of (VectQuot (V,W)) by Def6;
then w in { A where A is Coset of W : verum } ;
then ex A being Coset of W st A = w ;
hence ( w is Coset of W & ex v being Vector of V st w = v + W ) by VECTSP_4:def 6; :: thesis: verum