let V be RealLinearSpace; :: thesis: for v being VECTOR of V
for W being Subspace of V holds v in v + W
let v be VECTOR of V; :: thesis: for W being Subspace of V holds v in v + W
let W be Subspace of V; :: thesis: v in v + W
( v + (0. V) = v & 0. V in W ) by Th17;
hence v in v + W ; :: thesis: verum