let K be Field; :: thesis:
let V1 be finite-dimensional VectSp of K; :: thesis:
let b1 be OrdBasis of V1; :: thesis:
let J be FinSequence_of_Jordan_block of 0. K,K; :: thesis:
let M be Matrix of len b1, len b1,K; :: thesis:
assume that
A1: M = block_diagonal J,(0. K) and
A2: len b1 > 0 ; :: thesis:
set mm = min (Len J),(len b1);
A3: ( len M = len b1 & len M = Sum (Len J) & len b1 in Seg (len b1) & dom b1 = Seg (len b1) ) by A1, A2, FINSEQ_1:5, FINSEQ_1:def 3, MATRIX_1:def 3;
then A4: ( min (Len J),(len b1) in dom (Len J) & dom J = dom (Len J) ) by MATRIXJ1:def 1, MATRIXJ1:def 3;
let F be nilpotent Function of V1,V1; :: thesis:
assume A5: F = Mx2Tran M,b1,b1 ; :: thesis:
defpred S₁[ Nat] means for i being Nat st i in dom J holds
len (J . i) <= $1;

let i be Nat; :: thesis:
assume A6: i in dom J ; :: thesis:
len (J . i) = (Len J) . i by A4, A6, MATRIXJ1:def 3;
hence len (J . i) <= Sum (Len J) by A4, A6, POLYNOM3:4; :: thesis:

end;

then A7: ex k being Nat st S₁[k] ;
consider MIN being Nat such that
A8: S₁[MIN] and
A9: for m being Nat st S₁[m] holds
MIN <= m from NAT_1:sch 5(A7);
A10: ex i being Nat st
( i in dom J & len (J . i) = MIN )

assume A11: for i being Nat st i in dom J holds
len (J . i) <> MIN ; :: thesis:
then ( len (J . (min (Len J),(len b1))) <> MIN & len (J . (min (Len J),(len b1))) <= MIN ) by A4, A8;
then len (J . (min (Len J),(len b1))) < MIN by XXREAL_0:1;
then reconsider M1 = MIN - 1 as Element of NAT by NAT_1:20;

let i be Nat; :: thesis:
assume A12: i in dom J ; :: thesis:
( len (J . i) <> MIN & len (J . i) <= MIN ) by A8, A11, A12;
then len (J . i) < M1 + 1 by XXREAL_0:1;
hence len (J . i) <= M1 by NAT_1:13; :: thesis:

end;

then M1 + 1 <= M1 by A9;
hence contradiction by NAT_1:13; :: thesis:

end;

then consider i being Nat such that
A13: ( i in dom J & len (J . i) = MIN ) ;
A14: ( len (J . i) = (Len J) . i & (Len J) . i = (Len J) /. i ) by A4, A13, MATRIXJ1:def 3, PARTFUN1:def 8;
set S = Sum ((Len J) | (i -' 1));
( 1 <= i & i <= len (Len J) & i in NAT ) by A4, A13, FINSEQ_3:27;
then ( Sum ((Len J) | i) <= Sum ((Len J) | (len (Len J))) & (Len J) | (len (Len J)) = Len J & i -' 1 = i - 1 ) by FINSEQ_1:79, POLYNOM3:18, XREAL_1:235;
then A15: ( i = (i -' 1) + 1 & Seg (Sum ((Len J) | i)) c= Seg (Sum (Len J)) ) by FINSEQ_1:7;
defpred S₂[ Nat] means ( $1 in Seg MIN & $1 <> MIN implies (F |^ $1) . (b1 /. ((Sum ((Len J) | (i -' 1))) + 1)) = b1 /. (((Sum ((Len J) | (i -' 1))) + $1) + 1) );
A16: S₂[ 0 ] by FINSEQ_1:3;
A17: for n being Nat st S₂[n] holds
S₂[n + 1]

let n be Nat; :: thesis:
assume A18: S₂[n] ; :: thesis:
set n1 = n + 1;
assume A19: ( n + 1 in Seg MIN & n + 1 <> MIN ) ; :: thesis:
(Len J) | i = ((Len J) | (i -' 1)) ^ <*MIN*> by A4, A13, A14, A15, FINSEQ_5:11;
then A20: Sum ((Len J) | i) = (Sum ((Len J) | (i -' 1))) + MIN by RVSUM_1:104;
n + 1 <= MIN by A19, FINSEQ_1:3;
then A21: ( n + 1 < MIN & n < MIN ) by A19, NAT_1:13, XXREAL_0:1;
then A22: (Sum ((Len J) | (i -' 1))) + (n + 1) < Sum ((Len J) | i) by A20, XREAL_1:8;
( (Sum ((Len J) | (i -' 1))) + (n + 1) in Seg (Sum ((Len J) | i)) & min (Len J),((Sum ((Len J) | (i -' 1))) + (n + 1)) = i & (Len J) | i = Len (J | i) ) by A4, A13, A14, A19, MATRIXJ1:10, MATRIXJ1:17;
then A23: F . (b1 /. ((Sum ((Len J) | (i -' 1))) + (n + 1))) = ((0. K) * (b1 /. ((Sum ((Len J) | (i -' 1))) + (n + 1)))) + (b1 /. (((Sum ((Len J) | (i -' 1))) + (n + 1)) + 1)) by A1, A3, A5, A15, A22, Th24
.= (0. V1) + (b1 /. (((Sum ((Len J) | (i -' 1))) + (n + 1)) + 1)) by VECTSP_1:59
.= b1 /. (((Sum ((Len J) | (i -' 1))) + (n + 1)) + 1) by RLVECT_1:def 7 ;

per cases by NAT_1:14;

suppose n = 0 ; :: thesis:

hence (F |^ (n + 1)) . (b1 /. ((Sum ((Len J) | (i -' 1))) + 1)) = b1 /. (((Sum ((Len J) | (i -' 1))) + (n + 1)) + 1) by A23, VECTSP11:19; :: thesis:

end;

suppose A24: n >= 1 ; :: thesis:

end;

hence (F |^ (n + 1)) . (b1 /. ((Sum ((Len J) | (i -' 1))) + 1)) = b1 /. (((Sum ((Len J) | (i -' 1))) + (n + 1)) + 1) ; :: thesis:

end;

A26: for n being Nat holds S₂[n] from NAT_1:sch 2(A16, A17);
A27: deg F >= MIN

set D = deg F;
assume A28: deg F < MIN ; :: thesis:
deg F <> 0

assume deg F = 0 ; :: thesis:
then [#] V1 = {(0. V1)} by Th15;
then (Omega). V1 = (0). V1 by VECTSP_4:def 3;
then dim V1 = 0 by VECTSP_9:33;
hence contradiction by A2, MATRLIN2:21; :: thesis:

end;

then deg F >= 1 by NAT_1:14;
then deg F in Seg MIN by A28, FINSEQ_1:3;
then A29: b1 /. (((Sum ((Len J) | (i -' 1))) + (deg F)) + 1) = (F |^ (deg F)) . (b1 /. ((Sum ((Len J) | (i -' 1))) + 1)) by A28, A26
.= (ZeroMap V1,V1) . (b1 /. ((Sum ((Len J) | (i -' 1))) + 1)) by Def5
.= (the carrier of V1 --> (0. V1)) . (b1 /. ((Sum ((Len J) | (i -' 1))) + 1)) by GRCAT_1:def 12
.= 0. V1 by FUNCOP_1:13 ;
( 1 <= 1 + (deg F) & (deg F) + 1 <= MIN ) by A28, NAT_1:11, NAT_1:13;
then (deg F) + 1 in Seg MIN ;
then ( (Sum ((Len J) | (i -' 1))) + ((deg F) + 1) in Seg (Sum ((Len J) | i)) & rng b1 is Basis of V1 ) by A4, A13, A14, MATRIXJ1:10, MATRLIN:def 4;
then ( b1 /. (((Sum ((Len J) | (i -' 1))) + (deg F)) + 1) = b1 . (((Sum ((Len J) | (i -' 1))) + (deg F)) + 1) & b1 . (((Sum ((Len J) | (i -' 1))) + (deg F)) + 1) in rng b1 & rng b1 is linearly-independent Subset of V1 ) by A3, A15, FUNCT_1:def 5, PARTFUN1:def 8, VECTSP_7:def 3;
hence contradiction by A29, VECTSP_7:3; :: thesis:

end;

F |^ MIN = ZeroMap V1,V1 by A1, A5, A8, Th25;
then deg F <= MIN by Def5;
then deg F = MIN by A27, XXREAL_0:1;
hence ( ex i being Nat st
( i in dom J & len (J . i) = deg F ) & ( for i being Nat st i in dom J holds
len (J . i) <= deg F ) ) by A8, A10; :: thesis: