let F be Field; :: thesis:
let V be finite-dimensional VectSp of F; :: thesis:
let k be Nat; :: thesis:
assume that
A1: 1 <= k and
A2: k < dim V and
A3: 3 <= dim V ; :: thesis:
set S = PencilSpace (V,k);

let B be Block of (PencilSpace (V,k)); :: thesis:
not the topology of (PencilSpace (V,k)) is empty by A1, A2, Th11;
then consider W1, W2 being Subspace of V such that
A4: W1 is Subspace of W2 and
A5: (dim W1) + 1 = k and
A6: dim W2 = k + 1 and
A7: B = pencil (W1,W2,k) by Def4;
A8: the carrier of W1 c= the carrier of V by VECTSP_4:def 2;

per cases by A2, A3, Th1;

suppose k + 1 < dim V ; :: thesis:

then A9: (Omega). W2 <> (Omega). V by A6, VECTSP_9:28;

A10: now

assume A11: the carrier of V = the carrier of W2 ; :: thesis:
(Omega). W2 is Subspace of V by Th5;
hence contradiction by A9, A11, VECTSP_4:29; :: thesis:

end;

the carrier of W2 c= the carrier of V by VECTSP_4:def 2;
then not the carrier of V c= the carrier of W2 by A10, XBOOLE_0:def 10;
then consider v being set such that
A12: v in the carrier of V and
A13: not v in the carrier of W2 by TARSKI:def 3;
reconsider v = v as Vector of V by A12;
set X = W1 + (Lin {v});

A14: now

v in {v} by TARSKI:def 1;
then v in Lin {v} by VECTSP_7:8;
then v in W1 + (Lin {v}) by VECTSP_5:2;
then A15: v in the carrier of (W1 + (Lin {v})) by STRUCT_0:def 5;
assume W1 + (Lin {v}) in B ; :: thesis:
then W1 + (Lin {v}) is Subspace of W2 by A7, Th9;
then the carrier of (W1 + (Lin {v})) c= the carrier of W2 by VECTSP_4:def 2;
hence contradiction by A13, A15; :: thesis:

end;

not v in W2 by A13, STRUCT_0:def 5;
then dim (W1 + (Lin {v})) = k by A4, A5, Th14, VECTSP_4:8;
hence the carrier of (PencilSpace (V,k)) <> B by A14, VECTSP_9:def 2; :: thesis:

end;

suppose A16: ( 2 <= k & k + 1 >= dim V ) ; :: thesis:

set I = the Basis of W1;
reconsider I1 = the Basis of W1 as finite Subset of W1 by VECTSP_9:20;
2 - 1 <= ((dim W1) + 1) - 1 by A5, A16, XREAL_1:9;
then 1 <= card I1 by VECTSP_9:def 1;
then not I1 is empty ;
then consider i being set such that
A17: i in the Basis of W1 by XBOOLE_0:def 1;
reconsider i = i as Vector of W1 by A17;
reconsider J = I1 \ {i} as finite Subset of V by A8, XBOOLE_1:1;
the Basis of W1 is linearly-independent by VECTSP_7:def 3;
then the Basis of W1 \ {i} is linearly-independent by VECTSP_7:1, XBOOLE_1:36;
then reconsider JJ = the Basis of W1 \ {i} as linearly-independent Subset of V by VECTSP_9:11;
J c= the carrier of (Lin J)

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in J ; :: thesis:
then a in Lin J by VECTSP_7:8;
hence a in the carrier of (Lin J) by STRUCT_0:def 5; :: thesis:

end;

then reconsider JJJ = JJ as linearly-independent Subset of (Lin J) by VECTSP_9:12;
Lin JJJ = Lin J by VECTSP_9:17;
then A18: J is Basis of Lin J by VECTSP_7:def 3;
A19: card the Basis of W1 = dim W1 by VECTSP_9:def 1;
set T = the Linear_Compl of W1;
A20: V is_the_direct_sum_of W1, the Linear_Compl of W1 by VECTSP_5:38;
then A21: W1 /\ the Linear_Compl of W1 = (0). V by VECTSP_5:def 4;
k + 1 <= dim V by A2, NAT_1:13;
then dim V = k + 1 by A16, XXREAL_0:1;
then (k + 1) - ((dim W1) + 1) = ((dim W1) + (dim the Linear_Compl of W1)) - ((dim W1) + 1) by A20, VECTSP_9:34;
then consider u, v being Vector of the Linear_Compl of W1 such that
A22: u <> v and
A23: {u,v} is linearly-independent and
A24: (Omega). the Linear_Compl of W1 = Lin {u,v} by A5, VECTSP_9:31;
A25: v in the carrier of the Linear_Compl of W1 ;
( the carrier of the Linear_Compl of W1 c= the carrier of V & u in the carrier of the Linear_Compl of W1 ) by VECTSP_4:def 2;
then reconsider u1 = u, v1 = v as Vector of V by A25;
reconsider Y = {u,v} as linearly-independent Subset of V by A23, VECTSP_9:11;
A26: Y = {u,v} ;
Lin ( the Basis of W1 \ {i}) is Subspace of Lin the Basis of W1 by VECTSP_7:13, XBOOLE_1:36;
then A27: Lin J is Subspace of W1 by VECTSP_9:17;
the carrier of ((Lin J) /\ (Lin {u1,v1})) c= the carrier of ((0). V)

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in the carrier of ((Lin J) /\ (Lin {u1,v1})) ; :: thesis:
then A28: a in (Lin J) /\ (Lin {u1,v1}) by STRUCT_0:def 5;
then a in Lin {u1,v1} by VECTSP_5:3;
then a in Lin {u,v} by VECTSP_9:17;
then a in the carrier of VectSpStr(# the carrier of the Linear_Compl of W1, the U5 of the Linear_Compl of W1, the ZeroF of the Linear_Compl of W1, the lmult of the Linear_Compl of W1 #) by A24, STRUCT_0:def 5;
then A29: a in the Linear_Compl of W1 by STRUCT_0:def 5;
a in Lin J by A28, VECTSP_5:3;
then a in W1 by A27, VECTSP_4:8;
then a in W1 /\ the Linear_Compl of W1 by A29, VECTSP_5:3;
hence a in the carrier of ((0). V) by A21, STRUCT_0:def 5; :: thesis:

end;

then A30: ( (0). V is Subspace of (Lin J) /\ (Lin {u1,v1}) & (Lin J) /\ (Lin {u1,v1}) is Subspace of (0). V ) by VECTSP_4:27, VECTSP_4:39;
card J = (card I1) - (card {i}) by A17, EULER_1:4
.= (dim W1) - 1 by A19, CARD_1:30 ;
then dim (Lin J) = (dim W1) - 1 by A18, VECTSP_9:def 1;
then A31: dim ((Lin J) + (Lin {u1,v1})) = ((dim W1) - 1) + 2 by A22, A26, A30, Th15, VECTSP_4:25;
A32: Lin the Basis of W1 = (Omega). W1 by VECTSP_7:def 3;
A33: i in W1 by STRUCT_0:def 5;

A34: now

reconsider IV = the Basis of W1 as Subset of V by A8, XBOOLE_1:1;
assume A35: i in (Lin J) + (Lin {u1,v1}) ; :: thesis:
IV c= the carrier of ((Lin J) + (Lin {u1,v1}))

let a be set ; :: according to TARSKI:def 3 :: thesis:
{i} c= the Basis of W1 by A17, ZFMISC_1:31;
then A36: ( the Basis of W1 \ {i}) \/ {i} = the Basis of W1 by XBOOLE_1:45;
assume A37: a in IV ; :: thesis:

per cases by A37, A36, XBOOLE_0:def 3;

suppose a in J ; :: thesis:

then A38: a in Lin J by VECTSP_7:8;
then a in V by VECTSP_4:9;
then reconsider o = a as Vector of V by STRUCT_0:def 5;
o in (Lin J) + (Lin {u1,v1}) by A38, VECTSP_5:2;
hence a in the carrier of ((Lin J) + (Lin {u1,v1})) by STRUCT_0:def 5; :: thesis:

end;

suppose a in {i} ; :: thesis:

then a = i by TARSKI:def 1;
hence a in the carrier of ((Lin J) + (Lin {u1,v1})) by A35, STRUCT_0:def 5; :: thesis:

end;

end;

end;

then Lin IV is Subspace of (Lin J) + (Lin {u1,v1}) by VECTSP_9:16;
then Lin the Basis of W1 is Subspace of (Lin J) + (Lin {u1,v1}) by VECTSP_9:17;
then A39: W1 is Subspace of (Lin J) + (Lin {u1,v1}) by A32, Th6;
the carrier of (W1 /\ (Lin {u1,v1})) c= the carrier of ((0). V)

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in the carrier of (W1 /\ (Lin {u1,v1})) ; :: thesis:
then A40: a in W1 /\ (Lin {u1,v1}) by STRUCT_0:def 5;
then a in Lin {u1,v1} by VECTSP_5:3;
then a in Lin {u,v} by VECTSP_9:17;
then a in the carrier of VectSpStr(# the carrier of the Linear_Compl of W1, the U5 of the Linear_Compl of W1, the ZeroF of the Linear_Compl of W1, the lmult of the Linear_Compl of W1 #) by A24, STRUCT_0:def 5;
then A41: a in the Linear_Compl of W1 by STRUCT_0:def 5;
a in W1 by A40, VECTSP_5:3;
then a in W1 /\ the Linear_Compl of W1 by A41, VECTSP_5:3;
hence a in the carrier of ((0). V) by A21, STRUCT_0:def 5; :: thesis:

end;

then ( (0). V is Subspace of W1 /\ (Lin {u1,v1}) & W1 /\ (Lin {u1,v1}) is Subspace of (0). V ) by VECTSP_4:27, VECTSP_4:39;
then A42: dim (W1 + (Lin {u1,v1})) = (dim W1) + 2 by A22, A26, Th15, VECTSP_4:25;
Lin {u1,v1} is Subspace of (Lin J) + (Lin {u1,v1}) by VECTSP_5:7;
then W1 + (Lin {u1,v1}) is Subspace of (Lin J) + (Lin {u1,v1}) by A39, VECTSP_5:34;
then ((dim W1) + 1) + 1 <= (dim W1) + 1 by A31, A42, VECTSP_9:25;
hence contradiction by NAT_1:13; :: thesis:

end;

assume (Lin J) + (Lin {u1,v1}) in B ; :: thesis:
then W1 is Subspace of (Lin J) + (Lin {u1,v1}) by A7, Th9;
hence contradiction by A33, A34, VECTSP_4:8; :: thesis:

end;

hence the carrier of (PencilSpace (V,k)) <> B by A5, A31, VECTSP_9:def 2; :: thesis:

end;

end;

end;

then the carrier of (PencilSpace (V,k)) is not Block of (PencilSpace (V,k)) ;
hence not PencilSpace (V,k) is degenerated by PENCIL_1:def 5; :: thesis: