let R be Ring; :: thesis: for V being LeftMod of R
for W1, W2 being Subspace of V
for W1s, W2s being strict Subspace of V st W1s = (Omega). W1 & W2s = (Omega). W2 holds
W1s + W2s = W1 + W2
let V be LeftMod of R; :: thesis: for W1, W2 being Subspace of V
for W1s, W2s being strict Subspace of V st W1s = (Omega). W1 & W2s = (Omega). W2 holds
W1s + W2s = W1 + W2
let W1, W2 be Subspace of V; :: thesis: for W1s, W2s being strict Subspace of V st W1s = (Omega). W1 & W2s = (Omega). W2 holds
W1s + W2s = W1 + W2
let W1s, W2s be strict Subspace of V; :: thesis: ( W1s = (Omega). W1 & W2s = (Omega). W2 implies W1s + W2s = W1 + W2 )
assume A1: ( W1s = (Omega). W1 & W2s = (Omega). W2 ) ; :: thesis: W1s + W2s = W1 + W2
for x being Vector of V holds
( x in W1 + W2 iff x in W1s + W2s )

proof

let x be Vector of V; :: thesis: ( x in W1 + W2 iff x in W1s + W2s )

hereby :: thesis: ( x in W1s + W2s implies x in W1 + W2 )

assume x in W1 + W2 ; :: thesis: x in W1s + W2s
then consider x1, x2 being Vector of V such that
B1: ( x1 in W1 & x2 in W2 & x = x1 + x2 ) by VECTSP_5:1;
B2: x1 in W1s by A1, B1;
x2 in W2s by A1, B1;
hence x in W1s + W2s by B1, B2, VECTSP_5:1; :: thesis: verum

end;

assume x in W1s + W2s ; :: thesis: x in W1 + W2
then consider x1, x2 being Vector of V such that
B1: ( x1 in W1s & x2 in W2s & x = x1 + x2 ) by VECTSP_5:1;
B2: x1 in W1 by A1, B1;
x2 in W2 by A1, B1;
hence x in W1 + W2 by B1, B2, VECTSP_5:1; :: thesis: verum

end;

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