theorem Th13: :: PENCIL_4:13

for F being Field
for V being finite-dimensional VectSp of F
for W being Subspace of V
for v being Vector of V st not v in W holds
dim (W + (Lin {v})) = (dim W) + 1