let V be RealUnitarySpace; :: 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

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. V) & 0. V in W2 ) by RLVECT_1:4, RUSUB_1:11;
hence v in W1 + W2 by A2, Th1; :: thesis: verum

end;

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

( v = (0. V) + v & 0. V in W1 ) by RLVECT_1:4, RUSUB_1:11;
hence v in W1 + W2 by A3, Th1; :: thesis: verum

end;

end;

end;

hence v in W1 + W2 ; :: thesis: verum