theorem Th13: :: HAHNBAN:13

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})) st w in X holds
w |-- (W,(Lin {y})) = [w,(0. V)]