let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for v1, v2 being Element of V
for W being Subspace of V holds
( ex C being Coset of W st
( v1 in C & v2 in C ) iff v1 - v2 in W )
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for v1, v2 being Element of V
for W being Subspace 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 Element of V; :: thesis: for W being Subspace of V holds
( ex C being Coset of W st
( v1 in C & v2 in C ) iff v1 - v2 in W )
let W be Subspace 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 Element of V st C = v + W by Def6;
hence v1 - v2 in W by A1, Th63; :: 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 Element of V such that
A2: ( v1 in v + W & v2 in v + W ) by Th63;
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