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 v being Vector of V holds
( v + W is Coset of W & v + W is Vector of (VectQuot (V,W)) )
let V be VectSp of K; :: thesis: for W being Subspace of V
for v being Vector of V holds
( v + W is Coset of W & v + W is Vector of (VectQuot (V,W)) )
let W be Subspace of V; :: thesis: for v being Vector of V holds
( v + W is Coset of W & v + W is Vector of (VectQuot (V,W)) )
let v be Vector of V; :: thesis: ( v + W is Coset of W & v + W is Vector of (VectQuot (V,W)) )
set cs = CosetSet (V,W);
thus v + W is Coset of W by VECTSP_4:def 6; :: thesis: v + W is Vector of (VectQuot (V,W))
then v + W in CosetSet (V,W) ;
hence v + W is Vector of (VectQuot (V,W)) by Def6; :: thesis: verum