let R be Ring; :: thesis: for V being LeftMod of R
for W being Subspace of V
for Ws being strict Subspace of V
for A being object st Ws = (Omega). W holds
( A is Coset of W iff A is Coset of Ws )
let V be LeftMod of R; :: thesis: for W being Subspace of V
for Ws being strict Subspace 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 Subspace of V; :: thesis: for Ws being strict Subspace 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 Subspace 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