for K being Field
for V being VectSp of K
for v being Vector of V
for X being Subspace of V st not v in X holds
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y}