let V be Z_Module; :: thesis: for W being Submodule of V
for Ws being strict Submodule of V
for v being VECTOR of V st Ws = (Omega). W holds
v + W = v + Ws
let W be Submodule of V; :: thesis: for Ws being strict Submodule of V
for v being VECTOR of V st Ws = (Omega). W holds
v + W = v + Ws
let Ws be strict Submodule of V; :: thesis: for v being VECTOR of V st Ws = (Omega). W holds
v + W = v + Ws
let v be VECTOR of V; :: thesis: ( Ws = (Omega). W implies v + W = v + Ws )
assume A1: Ws = (Omega). W ; :: thesis: v + W = v + Ws
for x being object holds
( x in v + W iff x in v + Ws )

proof

let x be object ; :: thesis: ( x in v + W iff x in v + Ws )

hereby :: thesis: ( x in v + Ws implies x in v + W )

assume B1: x in v + W ; :: thesis: x in v + Ws
then reconsider xx = x as VECTOR of V ;
consider u being VECTOR of V such that
B2: ( u in W & xx = v + u ) by B1, ZMODUL01:72;
u in Ws by A1, B2;
hence x in v + Ws by B2; :: thesis: verum

end;

assume B1: x in v + Ws ; :: thesis: x in v + W
then reconsider xx = x as VECTOR of V ;
consider u being VECTOR of V such that
B2: ( u in Ws & xx = v + u ) by B1, ZMODUL01:72;
u in W by A1, B2;
hence x in v + W by B2; :: thesis: verum

end;

hence v + W = v + Ws by TARSKI:2; :: thesis: verum