for F being Field
for V being finite-dimensional VectSp of F
for W1, W2 being Subspace of V st W1 is Subspace of W2 holds
for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
for v being Vector of V st v in W2 & not v in W1 holds
W1 + (Lin {v}) in pencil (W1,W2,k)