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 v being Vector of V st Ws = (Omega). W holds
v + W = v + Ws
let V be LeftMod of R; :: thesis: for W being Subspace of V
for Ws being strict Subspace of V
for v being Vector of V st Ws = (Omega). W holds
v + W = v + Ws
let W be Subspace of V; :: thesis: for Ws being strict Subspace of V
for v being Vector of V st Ws = (Omega). W holds
v + W = v + Ws
let Ws be strict Subspace 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: ( xx = v + u & u in W ) by B1;
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: ( xx = v + u & u in Ws ) by B1;
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