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
now :: thesis: v in W1 + W2
per cases ( v in W1 or v in W2 ) by A1;
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;
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;
end;
end;
hence v in W1 + W2 ; :: thesis: verum