let V be Z_Module; :: thesis: for W being Submodule of V
for Ws being strict Submodule of V st Ws = (Omega). W holds
CosetSet (V,W) = CosetSet (V,Ws)
let W be Submodule of V; :: thesis: for Ws being strict Submodule of V st Ws = (Omega). W holds
CosetSet (V,W) = CosetSet (V,Ws)
let Ws be strict Submodule 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