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 )

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

hence
W1 + W2 = W1s + W2s
by VECTSP_4:30; :: thesis: verum
let x be Vector of V; :: thesis: ( x in W1 + W2 iff x in W1s + W2s )

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;hereby :: thesis: ( x in W1s + W2s implies x in W1 + W2 )

assume
x in W1s + W2s
; :: thesis: x in W1 + W2assume
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;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

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