let V be RealUnitarySpace; :: thesis: for W being Subspace of V
for v being VECTOR of V holds v in v + W
let W be Subspace of V; :: thesis: for v being VECTOR of V holds v in v + W
let v be VECTOR of V; :: thesis: v in v + W
( v + (0. V) = v & 0. V in W ) by Th11, RLVECT_1:4;
hence v in v + W ; :: thesis: verum