let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M

for v being Element of M st ( v in W1 or v in W2 ) holds

v in W1 + W2

let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for W1, W2 being Subspace of M

for v being Element of M st ( v in W1 or v in W2 ) holds

v in W1 + W2

let W1, W2 be Subspace of M; :: thesis: for v being Element of M st ( v in W1 or v in W2 ) holds

v in W1 + W2

let v be Element of M; :: thesis: ( ( v in W1 or v in W2 ) implies v in W1 + W2 )

assume A1: ( v in W1 or v in W2 ) ; :: thesis: v in W1 + W2

for W1, W2 being Subspace of M

for v being Element of M st ( v in W1 or v in W2 ) holds

v in W1 + W2

let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for W1, W2 being Subspace of M

for v being Element of M st ( v in W1 or v in W2 ) holds

v in W1 + W2

let W1, W2 be Subspace of M; :: thesis: for v being Element of M st ( v in W1 or v in W2 ) holds

v in W1 + W2

let v be Element of M; :: thesis: ( ( v in W1 or v in W2 ) implies v in W1 + W2 )

assume A1: ( v in W1 or v in W2 ) ; :: thesis: v in W1 + W2

now :: thesis: v in W1 + W2end;

hence
v in W1 + W2
; :: thesis: verumper cases
( v in W1 or v in W2 )
by A1;

end;

suppose A2:
v in W1
; :: thesis: v in W1 + W2

( v = v + (0. M) & 0. M in W2 )
by RLVECT_1:4, VECTSP_4:17;

hence v in W1 + W2 by A2, Th1; :: thesis: verum

end;hence v in W1 + W2 by A2, Th1; :: thesis: verum

suppose A3:
v in W2
; :: thesis: v in W1 + W2

( v = (0. M) + v & 0. M in W1 )
by RLVECT_1:4, VECTSP_4:17;

hence v in W1 + W2 by A3, Th1; :: thesis: verum

end;hence v in W1 + W2 by A3, Th1; :: thesis: verum