theorem Th11: :: HAHNBAN:11

for V being RealLinearSpace
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}