let R be Ring; :: thesis: for V being LeftMod of R
for W being Subspace of V
for Ws being strict Subspace of V st Ws = (Omega). W holds
CosetSet (V,W) = CosetSet (V,Ws)
let V be LeftMod of R; :: thesis: for W being Subspace of V
for Ws being strict Subspace of V st Ws = (Omega). W holds
CosetSet (V,W) = CosetSet (V,Ws)
let W be Subspace of V; :: thesis: for Ws being strict Subspace of V st Ws = (Omega). W holds
CosetSet (V,W) = CosetSet (V,Ws)
let Ws be strict Subspace of V; :: thesis: ( Ws = (Omega). W implies CosetSet (V,W) = CosetSet (V,Ws) )
assume A1: Ws = (Omega). W ; :: thesis: CosetSet (V,W) = CosetSet (V,Ws)
for A being object holds
( A in CosetSet (V,W) iff A in CosetSet (V,Ws) )

proof

let A be object ; :: thesis: ( A in CosetSet (V,W) iff A in CosetSet (V,Ws) )

hereby :: thesis: ( A in CosetSet (V,Ws) implies A in CosetSet (V,W) )

assume A in CosetSet (V,W) ; :: thesis: A in CosetSet (V,Ws)
then consider AA being Coset of W such that
C1: A = AA ;
AA is Coset of Ws by A1, LmStrict11;
hence A in CosetSet (V,Ws) by C1; :: thesis: verum

end;

assume A in CosetSet (V,Ws) ; :: thesis: A in CosetSet (V,W)
then consider AA being Coset of Ws such that
C1: A = AA ;
AA is Coset of W by A1, LmStrict11;
hence A in CosetSet (V,W) by C1; :: thesis: verum

end;

hence CosetSet (V,W) = CosetSet (V,Ws) by TARSKI:2; :: thesis: verum