let V be RealLinearSpace; :: thesis: for W1, W2 being Subspace of V

for v being VECTOR of V st ( v in W1 or v in W2 ) holds

v in W1 + W2

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

v in W1 + W2

let v be VECTOR of V; :: 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 v being VECTOR of V st ( v in W1 or v in W2 ) holds

v in W1 + W2

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

v in W1 + W2

let v be VECTOR of V; :: 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: verum