let F be Field; :: thesis: 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
not pencil W1,W2,k is trivial
let V be finite-dimensional VectSp of F; :: thesis: 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
not pencil W1,W2,k is trivial
let W1, W2 be Subspace of V; :: thesis: ( W1 is Subspace of W2 implies for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
not pencil W1,W2,k is trivial )
assume W1 is Subspace of W2 ; :: thesis: for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
not pencil W1,W2,k is trivial
then reconsider U = W1 as Subspace of W2 ;
let k be Nat; :: thesis: ( (dim W1) + 1 = k & dim W2 = k + 1 implies not pencil W1,W2,k is trivial )
assume A1: ( (dim W1) + 1 = k & dim W2 = k + 1 ) ; :: thesis: not pencil W1,W2,k is trivial
consider W being Linear_Compl of U;
A2: W2 is_the_direct_sum_of W,U by VECTSP_5:def 5;
then A3: W /\ U = (0). W2 by VECTSP_5:def 4;
dim W2 = (dim U) + (dim W) by A2, VECTSP_9:38;
then consider u, v being Vector of W such that
A4: u <> v and
A5: {u,v} is linearly-independent and
(Omega). W = Lin {u,v} by A1, VECTSP_9:35;

A6: now

assume v in Lin {u} ; :: thesis: contradiction
then ex a being Element of F st v = a * u by VECTSP10:4;
hence contradiction by A4, A5, VECTSP_7:8; :: thesis: verum

end;

reconsider u = u, v = v as Vector of W2 by VECTSP_4:18;
reconsider u1 = u, v1 = v as Vector of V by VECTSP_4:18;
A7: v in W by STRUCT_0:def 5;

A8: now

assume v in W1 ; :: thesis: contradiction
then v in (0). W2 by A3, A7, VECTSP_5:7;
then v = 0. W2 by VECTSP_4:46;
then v = 0. W by VECTSP_4:19;
hence contradiction by A5, VECTSP_7:6; :: thesis: verum

end;

A9: u in W by STRUCT_0:def 5;

A10: now

assume u in W1 ; :: thesis: contradiction
then u in (0). W2 by A3, A9, VECTSP_5:7;
then u = 0. W2 by VECTSP_4:46;
then u = 0. W by VECTSP_4:19;
hence contradiction by A5, VECTSP_7:6; :: thesis: verum

end;

v in {v1} by TARSKI:def 1;
then v in Lin {v1} by VECTSP_7:13;
then A11: v in W1 + (Lin {v1}) by VECTSP_5:6;
A12: not v in Lin {u} by A6, VECTSP10:14;

A13: now

reconsider Wx = W as Subspace of V by VECTSP_4:34;
assume W1 + (Lin {v1}) = W1 + (Lin {u1}) ; :: thesis: contradiction
then consider h, j being Vector of V such that
A14: h in W1 and
A15: j in Lin {u1} and
A16: v1 = h + j by A11, VECTSP_5:5;
consider a being Element of F such that
A17: j = a * u1 by A15, VECTSP10:4;
v1 - (a * u1) = h + ((a * u1) - (a * u1)) by A16, A17, RLVECT_1:def 6;
then v1 - (a * u1) = h + (0. V) by RLVECT_1:28;
then A18: v1 - (a * u1) = h by RLVECT_1:10;
a * u = a * u1 by VECTSP_4:22;
then A19: v1 - (a * u1) = v - (a * u) by VECTSP_4:24;
a * u in Wx by A9, VECTSP_4:29;
then v - (a * u) in Wx by A7, VECTSP_4:31;
then v - (a * u) in W /\ U by A14, A18, A19, VECTSP_5:7;
then v - (a * u) = 0. W2 by A3, VECTSP_4:46;
then h = 0. V by A18, A19, VECTSP_4:19;
then v1 = j by A16, RLVECT_1:10;
hence contradiction by A12, A15, VECTSP10:14; :: thesis: verum

end;

v in W2 by STRUCT_0:def 5;
then A20: W1 + (Lin {v1}) in pencil W1,W2,k by A1, A8, Th16;
u in W2 by STRUCT_0:def 5;
then W1 + (Lin {u1}) in pencil W1,W2,k by A1, A10, Th16;
then 2 c= card (pencil W1,W2,k) by A13, A20, PENCIL_1:2;
hence not pencil W1,W2,k is trivial by PENCIL_1:4; :: thesis: verum