let K be algebraic-closed Field; :: thesis:
defpred S₁[ Nat] means for V being non trivial finite-dimensional VectSp of K st dim V <= $1 holds
for F being linear-transformation of V,V ex J being non-empty FinSequence_of_Jordan_block of K ex b1 being OrdBasis of V st
( AutMt (F,b1,b1) = block_diagonal (J,(0. K)) & ( for L being Scalar of K holds
( L is eigenvalue of F iff ex i being Nat st
( i in dom J & J . i = Jordan_block (L,(len (J . i))) ) ) ) );
let V be non trivial finite-dimensional VectSp of K; :: thesis:
let F be linear-transformation of V,V; :: thesis:
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume A2: S₁[n] ; :: thesis:
set n1 = n + 1;
let V be non trivial finite-dimensional VectSp of K; :: thesis:
assume A3: dim V <= n + 1 ; :: thesis:

per cases by A3, NAT_1:8;

suppose dim V <= n ; :: thesis:

hence for F being linear-transformation of V,V ex J being non-empty FinSequence_of_Jordan_block of K ex b1 being OrdBasis of V st
( AutMt (F,b1,b1) = block_diagonal (J,(0. K)) & ( for L being Scalar of K holds
( L is eigenvalue of F iff ex i being Nat st
( i in dom J & J . i = Jordan_block (L,(len (J . i))) ) ) ) ) by A2; :: thesis:

end;

suppose A4: dim V = n + 1 ; :: thesis:

let F be linear-transformation of V,V; :: thesis:
A5: F is with_eigenvalues by VECTSP11:16;
then consider v being Vector of V, L being Scalar of K such that
A6: ( v <> 0. V & F . v = L * v ) by VECTSP11:def 1;
set FL = F + ((- L) * (id V));
L is eigenvalue of F by A5, A6, VECTSP11:def 2;
then not ker (F + ((- L) * (id V))) is trivial by A5, VECTSP11:14;
then A7: dim (ker (F + ((- L) * (id V)))) <> 0 by MATRLIN2:42;
consider m being Nat such that
A8: UnionKers (F + ((- L) * (id V))) = ker ((F + ((- L) * (id V))) |^ m) by VECTSP11:27;
set IM = im ((F + ((- L) * (id V))) |^ m);
set KER = ker ((F + ((- L) * (id V))) |^ m);
A9: dim V = (dim (ker ((F + ((- L) * (id V))) |^ m))) + (dim (im ((F + ((- L) * (id V))) |^ m))) by A8, VECTSP11:35, VECTSP_9:34;
A10: im ((F + ((- L) * (id V))) |^ m) is Linear_Compl of ker ((F + ((- L) * (id V))) |^ m) by A8, VECTSP11:35, VECTSP_5:37;
reconsider FK = F | (ker ((F + ((- L) * (id V))) |^ m)) as linear-transformation of (ker ((F + ((- L) * (id V))) |^ m)),(ker ((F + ((- L) * (id V))) |^ m)) by VECTSP11:29;
consider Jk being non-empty FinSequence_of_Jordan_block of L,K, Bker being OrdBasis of ker ((F + ((- L) * (id V))) |^ m) such that
A11: AutMt (FK,Bker,Bker) = block_diagonal (Jk,(0. K)) by Th30;
(F + ((- L) * (id V))) |^ 1 = F + ((- L) * (id V)) by VECTSP11:19;
then A12: ker (F + ((- L) * (id V))) is Subspace of ker ((F + ((- L) * (id V))) |^ m) by A8, VECTSP11:25;
A13: len Jk <> 0

proof

assume len Jk = 0 ; :: thesis:
then Len Jk = <*> NAT
.= <*> REAL ;
then 0 = len (block_diagonal (Jk,(0. K))) by MATRIXJ1:def 5, RVSUM_1:72
.= len Bker by A11, MATRIX_0:def 2
.= dim (ker ((F + ((- L) * (id V))) |^ m)) by MATRLIN2:21 ;
hence contradiction by A12, A7, VECTSP_9:25; :: thesis:

end;

reconsider FI = F | (im ((F + ((- L) * (id V))) |^ m)) as linear-transformation of (im ((F + ((- L) * (id V))) |^ m)),(im ((F + ((- L) * (id V))) |^ m)) by VECTSP11:33;
A14: (ker ((F + ((- L) * (id V))) |^ m)) /\ (im ((F + ((- L) * (id V))) |^ m)) = (0). V by A8, VECTSP11:34;
A15: V is_the_direct_sum_of ker ((F + ((- L) * (id V))) |^ m), im ((F + ((- L) * (id V))) |^ m) by A8, VECTSP11:35;
then A16: (ker ((F + ((- L) * (id V))) |^ m)) + (im ((F + ((- L) * (id V))) |^ m)) = (Omega). V by VECTSP_5:def 4;

per cases ;

suppose A17: im ((F + ((- L) * (id V))) |^ m) is trivial ; :: thesis:

set Bim = the OrdBasis of im ((F + ((- L) * (id V))) |^ m);
0 = dim (im ((F + ((- L) * (id V))) |^ m)) by A17, MATRLIN2:42
.= len the OrdBasis of im ((F + ((- L) * (id V))) |^ m) by MATRLIN2:21
.= len (AutMt (FI, the OrdBasis of im ((F + ((- L) * (id V))) |^ m), the OrdBasis of im ((F + ((- L) * (id V))) |^ m))) by MATRIX_0:def 2 ;
then A18: AutMt (FI, the OrdBasis of im ((F + ((- L) * (id V))) |^ m), the OrdBasis of im ((F + ((- L) * (id V))) |^ m)) = {} ;
Bker ^ the OrdBasis of im ((F + ((- L) * (id V))) |^ m) is OrdBasis of (ker ((F + ((- L) * (id V))) |^ m)) + (im ((F + ((- L) * (id V))) |^ m)) by A14, MATRLIN2:26;
then reconsider BB = Bker ^ the OrdBasis of im ((F + ((- L) * (id V))) |^ m) as OrdBasis of V by A16, MATRLIN2:4;
take Jk ; :: thesis:
take BB ; :: thesis:
A19: ( dim (im ((F + ((- L) * (id V))) |^ m)) = 0 implies dim (im ((F + ((- L) * (id V))) |^ m)) = 0 ) ;
( dim (ker ((F + ((- L) * (id V))) |^ m)) = 0 implies dim (ker ((F + ((- L) * (id V))) |^ m)) = 0 ) ;
hence AutMt (F,BB,BB) = block_diagonal (<*(AutMt (FK,Bker,Bker)),(AutMt (FI, the OrdBasis of im ((F + ((- L) * (id V))) |^ m), the OrdBasis of im ((F + ((- L) * (id V))) |^ m)))*>,(0. K)) by A15, A19, MATRLIN2:27
.= block_diagonal (<*(AutMt (FK,Bker,Bker))*>,(0. K)) by A18, MATRIXJ1:40
.= block_diagonal (Jk,(0. K)) by A11, MATRIXJ1:34 ;
:: thesis:
let L1 be Scalar of K; :: thesis:
thus ( L1 is eigenvalue of F implies ex i being Nat st
( i in dom Jk & Jk . i = Jordan_block (L1,(len (Jk . i))) ) ) :: thesis:

proof

assume A20: L1 is eigenvalue of F ; :: thesis:
A21: L1 = L

proof

assume L <> L1 ; :: thesis:
then ( FI is with_eigenvalues & L1 is eigenvalue of FI ) by A5, A8, A10, A20, VECTSP11:39;
then ex v1 being Vector of (im ((F + ((- L) * (id V))) |^ m)) st
( v1 <> 0. (im ((F + ((- L) * (id V))) |^ m)) & FI . v1 = L1 * v1 ) by VECTSP11:def 2;
hence contradiction by A17; :: thesis:

end;

take i = len Jk; :: thesis:
i in Seg (len Jk) by A13, FINSEQ_1:3;
hence i in dom Jk by FINSEQ_1:def 3; :: thesis:
then ex k being Nat st Jk . i = Jordan_block (L,k) by Def3;
hence Jk . i = Jordan_block (L1,(len (Jk . i))) by A21, Def1; :: thesis:

end;

given i being Nat such that A22: i in dom Jk and
A23: Jk . i = Jordan_block (L1,(len (Jk . i))) ; :: thesis:
Jk . i <> {} by A22, FUNCT_1:def 9;
then len (Jk . i) in Seg (len (Jk . i)) by FINSEQ_1:3;
then [(len (Jk . i)),(len (Jk . i))] in [:(Seg (len (Jk . i))),(Seg (len (Jk . i))):] by ZFMISC_1:87;
then A24: [(len (Jk . i)),(len (Jk . i))] in Indices (Jk . i) by MATRIX_0:24;
ex k being Nat st Jk . i = Jordan_block (L,k) by A22, Def3;
then L = (Jk . i) * ((len (Jk . i)),(len (Jk . i))) by A24, Def1
.= L1 by A23, A24, Def1 ;
hence L1 is eigenvalue of F by A5, A6, VECTSP11:def 2; :: thesis:

end;

suppose A25: not im ((F + ((- L) * (id V))) |^ m) is trivial ; :: thesis:

( n + 1 <> dim (im ((F + ((- L) * (id V))) |^ m)) & dim (im ((F + ((- L) * (id V))) |^ m)) <= n + 1 ) by A4, A12, A7, A9, VECTSP_9:25;
then dim (im ((F + ((- L) * (id V))) |^ m)) < n + 1 by XXREAL_0:1;
then dim (im ((F + ((- L) * (id V))) |^ m)) <= n by NAT_1:13;
then consider Ji being non-empty FinSequence_of_Jordan_block of K, Bim being OrdBasis of im ((F + ((- L) * (id V))) |^ m) such that
A26: AutMt (FI,Bim,Bim) = block_diagonal (Ji,(0. K)) and
A27: for L being Scalar of K holds
( L is eigenvalue of FI iff ex i being Nat st
( i in dom Ji & Ji . i = Jordan_block (L,(len (Ji . i))) ) ) by A2, A25;
Bker ^ Bim is OrdBasis of (ker ((F + ((- L) * (id V))) |^ m)) + (im ((F + ((- L) * (id V))) |^ m)) by A14, MATRLIN2:26;
then reconsider BB = Bker ^ Bim as OrdBasis of V by A16, MATRLIN2:4;
set JJ = Jk ^ Ji;

A28: now :: thesis:

let x be object ; :: thesis:
assume A29: x in dom (Jk ^ Ji) ; :: thesis:
reconsider i = x as Nat by A29;

now :: thesis:

per cases by A29, FINSEQ_1:25;

suppose A30: i in dom Jk ; :: thesis:

then (Jk ^ Ji) . i = Jk . i by FINSEQ_1:def 7;
hence not (Jk ^ Ji) . i is empty by A30, FUNCT_1:def 9; :: thesis:

end;

suppose ex j being Nat st
( j in dom Ji & i = (len Jk) + j ) ; :: thesis:

then consider j being Nat such that
A31: j in dom Ji and
A32: i = (len Jk) + j ;
(Jk ^ Ji) . i = Ji . j by A31, A32, FINSEQ_1:def 7;
hence not (Jk ^ Ji) . i is empty by A31, FUNCT_1:def 9; :: thesis:

end;

hence not (Jk ^ Ji) . x is empty ; :: thesis:

end;

A33: FI is with_eigenvalues by A25, VECTSP11:16;
A34: ( dim (im ((F + ((- L) * (id V))) |^ m)) = 0 implies dim (im ((F + ((- L) * (id V))) |^ m)) = 0 ) ;
reconsider JJ = Jk ^ Ji as non-empty FinSequence_of_Jordan_block of K by A28, FUNCT_1:def 9;
take JJ ; :: thesis:
take BB ; :: thesis:
( dim (ker ((F + ((- L) * (id V))) |^ m)) = 0 implies dim (ker ((F + ((- L) * (id V))) |^ m)) = 0 ) ;
hence AutMt (F,BB,BB) = block_diagonal (<*(block_diagonal (Jk,(0. K))),(block_diagonal (Ji,(0. K)))*>,(0. K)) by A11, A15, A26, A34, MATRLIN2:27
.= block_diagonal ((<*(block_diagonal (Jk,(0. K)))*> ^ Ji),(0. K)) by MATRIXJ1:36
.= block_diagonal (JJ,(0. K)) by MATRIXJ1:35 ;
:: thesis:
let L1 be Scalar of K; :: thesis:
thus ( L1 is eigenvalue of F implies ex i being Nat st
( i in dom JJ & JJ . i = Jordan_block (L1,(len (JJ . i))) ) ) :: thesis:

proof

assume A35: L1 is eigenvalue of F ; :: thesis:

per cases ;

suppose A36: L = L1 ; :: thesis:

take i = len Jk; :: thesis:
A37: dom Jk c= dom JJ by FINSEQ_1:26;
i in Seg (len Jk) by A13, FINSEQ_1:3;
then A38: i in dom Jk by FINSEQ_1:def 3;
then ( ex k being Nat st Jk . i = Jordan_block (L,k) & JJ . i = Jk . i ) by Def3, FINSEQ_1:def 7;
hence ( i in dom JJ & JJ . i = Jordan_block (L1,(len (JJ . i))) ) by A36, A38, A37, Def1; :: thesis:

end;

suppose L <> L1 ; :: thesis:

then L1 is eigenvalue of FI by A5, A8, A10, A35, VECTSP11:39;
then consider i being Nat such that
A39: i in dom Ji and
A40: Ji . i = Jordan_block (L1,(len (Ji . i))) by A27;
take ii = (len Jk) + i; :: thesis:
JJ . ii = Ji . i by A39, FINSEQ_1:def 7;
hence ( ii in dom JJ & JJ . ii = Jordan_block (L1,(len (JJ . ii))) ) by A39, A40, FINSEQ_1:28; :: thesis:

end;

given i being Nat such that A41: i in dom JJ and
A42: JJ . i = Jordan_block (L1,(len (JJ . i))) ; :: thesis:

per cases by A41, FINSEQ_1:25;

suppose A43: i in dom Jk ; :: thesis:

then Jk . i <> {} by FUNCT_1:def 9;
then len (Jk . i) in Seg (len (Jk . i)) by FINSEQ_1:3;
then [(len (Jk . i)),(len (Jk . i))] in [:(Seg (len (Jk . i))),(Seg (len (Jk . i))):] by ZFMISC_1:87;
then A44: [(len (Jk . i)),(len (Jk . i))] in Indices (Jk . i) by MATRIX_0:24;
A45: JJ . i = Jk . i by A43, FINSEQ_1:def 7;
ex k being Nat st Jk . i = Jordan_block (L,k) by A43, Def3;
then L = (Jk . i) * ((len (Jk . i)),(len (Jk . i))) by A44, Def1
.= L1 by A42, A45, A44, Def1 ;
hence L1 is eigenvalue of F by A5, A6, VECTSP11:def 2; :: thesis:

end;

suppose ex j being Nat st
( j in dom Ji & i = (len Jk) + j ) ; :: thesis:

then consider j being Nat such that
A46: j in dom Ji and
A47: i = (len Jk) + j ;
JJ . i = Ji . j by A46, A47, FINSEQ_1:def 7;
then L1 is eigenvalue of FI by A27, A42, A46;
then consider w being Vector of (im ((F + ((- L) * (id V))) |^ m)) such that
A48: w <> 0. (im ((F + ((- L) * (id V))) |^ m)) and
A49: FI . w = L1 * w by A33, VECTSP11:def 2;
A50: 0. (im ((F + ((- L) * (id V))) |^ m)) = 0. V by VECTSP_4:11;
reconsider W = w as Vector of V by VECTSP_4:10;
L1 * W = FI . w by A49, VECTSP_4:14
.= F . W by FUNCT_1:49 ;
hence L1 is eigenvalue of F by A5, A48, A50, VECTSP11:def 2; :: thesis:

end;

A51: S₁[ 0 ]

proof

let V be non trivial finite-dimensional VectSp of K; :: thesis:
assume dim V <= 0 ; :: thesis:
then dim V = 0 ;
hence for F being linear-transformation of V,V ex J being non-empty FinSequence_of_Jordan_block of K ex b1 being OrdBasis of V st
( AutMt (F,b1,b1) = block_diagonal (J,(0. K)) & ( for L being Scalar of K holds
( L is eigenvalue of F iff ex i being Nat st
( i in dom J & J . i = Jordan_block (L,(len (J . i))) ) ) ) ) by MATRLIN2:42; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A51, A1);
then S₁[ dim V] ;
hence ex J being non-empty FinSequence_of_Jordan_block of K ex b1 being OrdBasis of V st
( AutMt (F,b1,b1) = block_diagonal (J,(0. K)) & ( for L being Scalar of K holds
( L is eigenvalue of F iff ex i being Nat st
( i in dom J & J . i = Jordan_block (L,(len (J . i))) ) ) ) ) ; :: thesis: