let R be Ring; :: thesis: for V being LeftMod of R
for W being Subspace of V
for W1s, W2s being Subspace of W
for W1, W2 being Subspace of V st W1s = W1 & W2s = W2 holds
W1s + W2s = W1 + W2
let V be LeftMod of R; :: thesis: for W being Subspace of V
for W1s, W2s being Subspace of W
for W1, W2 being Subspace of V st W1s = W1 & W2s = W2 holds
W1s + W2s = W1 + W2
let W be Subspace of V; :: thesis: for W1s, W2s being Subspace of W
for W1, W2 being Subspace of V st W1s = W1 & W2s = W2 holds
W1s + W2s = W1 + W2
let W1s, W2s be Subspace of W; :: thesis: for W1, W2 being Subspace of V st W1s = W1 & W2s = W2 holds
W1s + W2s = W1 + W2
let W1, W2 be Subspace 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 Subspace of V by VECTSP_4:26;
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 VECTSP_5:1;
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 VECTSP_4:13, B1;
hence v in W1 + W2 by VECTSP_5:1, 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 VECTSP_5:1;
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 VECTSP_4:13, B1;
hence v in SWs12 by AS, B1, VECTSP_5:1; :: thesis: verum

end;

hence W1s + W2s = W1 + W2 by VECTSP_4:30; :: thesis: verum