let R be Ring; :: thesis: for V being RightMod of R
for W being Submodule of V
for C being Coset of W holds
( 0. V in C iff C = the carrier of W )
let V be RightMod of R; :: thesis: for W being Submodule of V
for C being Coset of W holds
( 0. V in C iff C = the carrier of W )
let W be Submodule of V; :: thesis: for C being Coset of W holds
( 0. V in C iff C = the carrier of W )
let C be Coset of W; :: thesis: ( 0. V in C iff C = the carrier of W )
ex v being Vector of V st C = v + W by Def6;
hence ( 0. V in C iff C = the carrier of W ) by Th48; :: thesis: verum