let F be Field; :: thesis: for V being finite-dimensional VectSp of F
for k being Nat
for W1, W2, W being Subspace of V st W in pencil (W1,W2,k) holds
( W1 is Subspace of W & W is Subspace of W2 )
let V be finite-dimensional VectSp of F; :: thesis: for k being Nat
for W1, W2, W being Subspace of V st W in pencil (W1,W2,k) holds
( W1 is Subspace of W & W is Subspace of W2 )
let k be Nat; :: thesis: for W1, W2, W being Subspace of V st W in pencil (W1,W2,k) holds
( W1 is Subspace of W & W is Subspace of W2 )
let W1, W2, W be Subspace of V; :: thesis: ( W in pencil (W1,W2,k) implies ( W1 is Subspace of W & W is Subspace of W2 ) )
assume A1: W in pencil (W1,W2,k) ; :: thesis: ( W1 is Subspace of W & W is Subspace of W2 )
then A2: ex X being strict Subspace of V st
( W = X & dim X = k ) by VECTSP_9:def 2;
W in pencil (W1,W2) by A1, XBOOLE_0:def 4;
then A3: W in segment (W1,W2) by XBOOLE_0:def 5;
then W1 is Subspace of W2 by Def1;
hence ( W1 is Subspace of W & W is Subspace of W2 ) by A2, A3, Def1; :: thesis: verum