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 A being Coset of W holds A is Vector of (VectQuot (V,W))

let V be VectSp of K; :: thesis: for W being Subspace of V

for A being Coset of W holds A is Vector of (VectQuot (V,W))

let W be Subspace of V; :: thesis: for A being Coset of W holds A is Vector of (VectQuot (V,W))

let A be Coset of W; :: thesis: A is Vector of (VectQuot (V,W))

set cs = CosetSet (V,W);

A in CosetSet (V,W) ;

hence A is Vector of (VectQuot (V,W)) by Def6; :: thesis: verum

for W being Subspace of V

for A being Coset of W holds A is Vector of (VectQuot (V,W))

let V be VectSp of K; :: thesis: for W being Subspace of V

for A being Coset of W holds A is Vector of (VectQuot (V,W))

let W be Subspace of V; :: thesis: for A being Coset of W holds A is Vector of (VectQuot (V,W))

let A be Coset of W; :: thesis: A is Vector of (VectQuot (V,W))

set cs = CosetSet (V,W);

A in CosetSet (V,W) ;

hence A is Vector of (VectQuot (V,W)) by Def6; :: thesis: verum