:: deftheorem defines pencil PENCIL_4:def 3 :
for F being Field
for V being finite-dimensional VectSp of F
for W1, W2 being Subspace of V
for k being Nat holds pencil (W1,W2,k) = (pencil (W1,W2)) /\ (k Subspaces_of V);