let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; :: thesis: for V being VectSp of
for W being Subspace of V
for A being Coset of W holds A is Vector of
let V be VectSp of ; :: thesis: for W being Subspace of V
for A being Coset of W holds A is Vector of
let W be Subspace of V; :: thesis: for A being Coset of W holds A is Vector of
let A be Coset of W; :: thesis: A is Vector of
set cs = CosetSet V,W;
A in CosetSet V,W ;
hence A is Vector of by Def6; :: thesis: verum