theorem Th16: :: VECTSP10:16

for K being Field
for V being VectSp of K
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)]