let V be Z_Module; :: 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 Def13;
hence ( 0. V in C iff C = the carrier of W ) by Th62; :: thesis: verum