theorem Th15: :: HAHNBAN:15

for V being RealLinearSpace
for v being VECTOR of V
for X being Subspace of V
for y being VECTOR of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being VECTOR of (X + (Lin {v})) ex x being VECTOR of X ex r being Real st w |-- (W,(Lin {y})) = [x,(r * v)]