let V be Z_Module; :: thesis: for W being Submodule of V
for W1s, W2s being Submodule of W
for W1, W2 being Submodule of V st W1s = W1 & W2s = W2 holds
W1s + W2s = W1 + W2
let W be Submodule of V; :: thesis: for W1s, W2s being Submodule of W
for W1, W2 being Submodule of V st W1s = W1 & W2s = W2 holds
W1s + W2s = W1 + W2
let W1s, W2s be Submodule of W; :: thesis: for W1, W2 being Submodule of V st W1s = W1 & W2s = W2 holds
W1s + W2s = W1 + W2
let W1, W2 be Submodule of V; :: thesis: ( W1s = W1 & W2s = W2 implies W1s + W2s = W1 + W2 )
assume AS: ( W1s = W1 & W2s = W2 ) ; :: thesis: W1s + W2s = W1 + W2
reconsider SWs12 = W1s + W2s as strict Submodule of V by ZMODUL01:42;
for v being VECTOR of V holds
( v in SWs12 iff v in W1 + W2 )

proof

let v be VECTOR of V; :: thesis: ( v in SWs12 iff v in W1 + W2 )

hereby :: thesis: ( v in W1 + W2 implies v in SWs12 )

assume v in SWs12 ; :: thesis: v in W1 + W2
then consider x1, x2 being VECTOR of W such that
B1: ( x1 in W1s & x2 in W2s & v = x1 + x2 ) by ZMODUL01:92;
the carrier of W1 c= the carrier of V by VECTSP_4:def 2;
then reconsider xx1 = x1 as VECTOR of V by AS, B1;
the carrier of W2 c= the carrier of V by VECTSP_4:def 2;
then reconsider xx2 = x2 as VECTOR of V by AS, B1;
v = xx1 + xx2 by ZMODUL01:28, B1;
hence v in W1 + W2 by ZMODUL01:92, AS, B1; :: thesis: verum

end;

assume v in W1 + W2 ; :: thesis: v in SWs12
then consider x1, x2 being VECTOR of V such that
B1: ( x1 in W1 & x2 in W2 & v = x1 + x2 ) by ZMODUL01:92;
the carrier of W1s c= the carrier of W by VECTSP_4:def 2;
then reconsider xx1 = x1 as VECTOR of W by AS, B1;
the carrier of W2s c= the carrier of W by VECTSP_4:def 2;
then reconsider xx2 = x2 as VECTOR of W by AS, B1;
v = xx1 + xx2 by ZMODUL01:28, B1;
hence v in SWs12 by AS, B1, ZMODUL01:92; :: thesis: verum

end;

hence W1s + W2s = W1 + W2 by ZMODUL01:46; :: thesis: verum