let V be Z_Module; :: thesis: for W being Submodule of V
for Ws being strict Submodule of V
for A being object st Ws = (Omega). W holds
( A is Coset of W iff A is Coset of Ws )
let W be Submodule of V; :: thesis: for Ws being strict Submodule of V
for A being object st Ws = (Omega). W holds
( A is Coset of W iff A is Coset of Ws )
let Ws be strict Submodule of V; :: thesis: for A being object st Ws = (Omega). W holds
( A is Coset of W iff A is Coset of Ws )
let A be object ; :: thesis: ( Ws = (Omega). W implies ( A is Coset of W iff A is Coset of Ws ) )
assume A1: Ws = (Omega). W ; :: thesis: ( A is Coset of W iff A is Coset of Ws )

hereby :: thesis: ( A is Coset of Ws implies A is Coset of W )

assume A is Coset of W ; :: thesis: A is Coset of Ws
then consider v being VECTOR of V such that
B1: A = v + W by VECTSP_4:def 6;
A = v + Ws by A1, B1, LmStrict11a;
hence A is Coset of Ws by VECTSP_4:def 6; :: thesis: verum

end;

assume A is Coset of Ws ; :: thesis: A is Coset of W
then consider v being VECTOR of V such that
B1: A = v + Ws by VECTSP_4:def 6;
A = v + W by A1, B1, LmStrict11a;
hence A is Coset of W by VECTSP_4:def 6; :: thesis: verum