let R be Ring; :: thesis: for V being RightMod of R
for v1, v2 being Vector of V
for W being Submodule of V holds
( ex C being Coset of W st
( v1 in C & v2 in C ) iff v1 - v2 in W )
let V be RightMod of R; :: thesis: for v1, v2 being Vector of V
for W being Submodule of V holds
( ex C being Coset of W st
( v1 in C & v2 in C ) iff v1 - v2 in W )
let v1, v2 be Vector of V; :: thesis: for W being Submodule of V holds
( ex C being Coset of W st
( v1 in C & v2 in C ) iff v1 - v2 in W )
let W be Submodule of V; :: thesis: ( ex C being Coset of W st
( v1 in C & v2 in C ) iff v1 - v2 in W )
thus ( ex C being Coset of W st
( v1 in C & v2 in C ) implies v1 - v2 in W ) :: thesis: ( v1 - v2 in W implies ex C being Coset of W st
( v1 in C & v2 in C ) )

proof

given C being Coset of W such that A1: ( v1 in C & v2 in C ) ; :: thesis: v1 - v2 in W
ex v being Vector of V st C = v + W by Def6;
hence v1 - v2 in W by A1, Th60; :: thesis: verum

end;

assume v1 - v2 in W ; :: thesis: ex C being Coset of W st
( v1 in C & v2 in C )
then consider v being Vector of V such that
A2: ( v1 in v + W & v2 in v + W ) by Th60;
reconsider C = v + W as Coset of W by Def6;
take C ; :: thesis: ( v1 in C & v2 in C )
thus ( v1 in C & v2 in C ) by A2; :: thesis: verum