let V be Z_Module; :: 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 Def13;
hence v1 - v2 in W by A1, Th74; :: 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 Th74;
reconsider C = v + W as Coset of W by Def13;
take C ; :: thesis: ( v1 in C & v2 in C )
thus ( v1 in C & v2 in C ) by A2; :: thesis: verum