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 ) )

( 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

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

assume
v1 - v2 in W
; :: thesis: ex C being Coset of W st
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;ex v being Element of V st C = v + W by Def6;

hence v1 - v2 in W by A1, Th63; :: thesis: verum

( 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