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: ( W in pencil W1,W2 & W in k Subspaces_of V ) by XBOOLE_0:def 4;
consider X being strict Subspace of V such that
A3: ( W = X & dim X = k ) by A1, VECTSP_9:def 3;
A4: W in segment W1,W2 by A2, XBOOLE_0:def 5;
then W1 is Subspace of W2 by Def1;
hence ( W1 is Subspace of W & W is Subspace of W2 ) by A3, A4, Def1; :: thesis: verum