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)) ) ) ) );
A1: S₁[ 0 ]

proof

let V be non trivial finite-dimensional VectSp of K; :: thesis:
assume A2: dim V <= 0 ; :: thesis:
dim V = 0 by A2;
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;

A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

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

per cases by A5, 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 A4; :: thesis:

end;

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

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

proof

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

end;

A14: ( V is_the_direct_sum_of ker ((F + ((- L) * (id V))) |^ m), im ((F + ((- L) * (id V))) |^ m) & (ker ((F + ((- L) * (id V))) |^ m)) /\ (im ((F + ((- L) * (id V))) |^ m)) = (0). V ) by A9, VECTSP11:34, VECTSP11:35;
then A15: ( dim V = (dim (ker ((F + ((- L) * (id V))) |^ m))) + (dim (im ((F + ((- L) * (id V))) |^ m))) & (ker ((F + ((- L) * (id V))) |^ m)) + (im ((F + ((- L) * (id V))) |^ m)) = (Omega). V & im ((F + ((- L) * (id V))) |^ m) is Linear_Compl of ker ((F + ((- L) * (id V))) |^ m) ) by VECTSP_5:47, VECTSP_5:def 4, VECTSP_9:38;

per cases ;

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

consider Bim being OrdBasis of im ((F + ((- L) * (id V))) |^ m);
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 A15, MATRLIN2:4;
take Jk ; :: thesis:
take BB ; :: thesis:
0 = dim (im ((F + ((- L) * (id V))) |^ m)) by A16, MATRLIN2:42
.= len Bim by MATRLIN2:21
.= len (AutMt FI,Bim,Bim) by MATRIX_1:def 3 ;
then A17: AutMt FI,Bim,Bim = {} ;
( ( dim (ker ((F + ((- L) * (id V))) |^ m)) = 0 implies dim (ker ((F + ((- L) * (id V))) |^ m)) = 0 ) & ( dim (im ((F + ((- L) * (id V))) |^ m)) = 0 implies dim (im ((F + ((- L) * (id V))) |^ m)) = 0 ) ) ;
hence AutMt F,BB,BB = block_diagonal <*(AutMt FK,Bker,Bker),(AutMt FI,Bim,Bim)*>,(0. K) by A14, MATRLIN2:27
.= block_diagonal <*(AutMt FK,Bker,Bker)*>,(0. K) by A17, MATRIXJ1:40
.= block_diagonal Jk,(0. K) by A12, 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 A18: L1 is eigenvalue of F ; :: thesis:
take i = len Jk; :: thesis:
i in Seg (len Jk) by A13, FINSEQ_1:5;
hence A19: i in dom Jk by FINSEQ_1:def 3; :: thesis:
consider k being Nat such that
A20: Jk . i = Jordan_block L,k by A19, Def3;
L1 = L

proof

assume L <> L1 ; :: thesis:
then ( FI is with_eigenvalues & L1 is eigenvalue of FI ) by A7, A10, A9, A15, A18, VECTSP11:39;
then consider v1 being Vector of (im ((F + ((- L) * (id V))) |^ m)) such that
A21: ( v1 <> 0. (im ((F + ((- L) * (id V))) |^ m)) & FI . v1 = L1 * v1 ) by VECTSP11:def 2;
thus contradiction by A21, A16, STRUCT_0:def 19; :: thesis:

end;

hence Jk . i = Jordan_block L1,(len (Jk . i)) by A20, Def1; :: thesis:

end;

given i being Nat such that A22: ( i in dom Jk & Jk . i = Jordan_block L1,(len (Jk . i)) ) ; :: thesis:
consider k being Nat such that
A23: Jk . i = Jordan_block L,k by A22, Def3;
Jk . i <> {} by A22, FUNCT_1:def 15;
then len (Jk . i) in Seg (len (Jk . i)) by FINSEQ_1:5;
then [(len (Jk . i)),(len (Jk . i))] in [:(Seg (len (Jk . i))),(Seg (len (Jk . i))):] by ZFMISC_1:106;
then A24: [(len (Jk . i)),(len (Jk . i))] in Indices (Jk . i) by MATRIX_1:25;
then L = (Jk . i) * (len (Jk . i)),(len (Jk . i)) by A23, Def1
.= L1 by A22, A24, Def1 ;
hence L1 is eigenvalue of F by A7, A8, VECTSP11:def 2; :: thesis:

end;

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

then A26: FI is with_eigenvalues by VECTSP11:16;
( n + 1 <> dim (im ((F + ((- L) * (id V))) |^ m)) & dim (im ((F + ((- L) * (id V))) |^ m)) <= n + 1 ) by A6, A11, A15, NAT_1:11;
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
A27: AutMt FI,Bim,Bim = block_diagonal Ji,(0. K) and
A28: 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 A4, A25;
set JJ = Jk ^ Ji;

now

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

now

per cases by A29, FINSEQ_1:38;

suppose i in dom Jk ; :: thesis:

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

end;

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

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

end;

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

end;

then reconsider JJ = Jk ^ Ji as non-empty FinSequence_of_Jordan_block of K by FUNCT_1:def 15;
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 A15, MATRLIN2:4;
take JJ ; :: thesis:
take BB ; :: thesis:
( ( dim (ker ((F + ((- L) * (id V))) |^ m)) = 0 implies dim (ker ((F + ((- L) * (id V))) |^ m)) = 0 ) & ( dim (im ((F + ((- L) * (id V))) |^ m)) = 0 implies dim (im ((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 A12, A27, A14, 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 A31: L1 is eigenvalue of F ; :: thesis:

per cases ;

suppose A32: L = L1 ; :: thesis:

take i = len Jk; :: thesis:
i in Seg (len Jk) by A13, FINSEQ_1:5;
then A33: i in dom Jk by FINSEQ_1:def 3;
then consider k being Nat such that
A34: Jk . i = Jordan_block L,k by Def3;
( dom Jk c= dom JJ & k = len (Jk . i) & JJ . i = Jk . i ) by A33, A34, Def1, FINSEQ_1:39, FINSEQ_1:def 7;
hence ( i in dom JJ & JJ . i = Jordan_block L1,(len (JJ . i)) ) by A32, A33, A34; :: thesis:

end;

suppose L <> L1 ; :: thesis:

then L1 is eigenvalue of FI by A7, A10, A9, A15, A31, VECTSP11:39;
then consider i being Nat such that
A35: ( i in dom Ji & Ji . i = Jordan_block L1,(len (Ji . i)) ) by A28;
take ii = (len Jk) + i; :: thesis:
( ii in dom JJ & JJ . ii = Ji . i ) by A35, FINSEQ_1:41, FINSEQ_1:def 7;
hence ( ii in dom JJ & JJ . ii = Jordan_block L1,(len (JJ . ii)) ) by A35; :: thesis:

end;

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

per cases by A36, FINSEQ_1:38;

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

then A38: JJ . i = Jk . i by FINSEQ_1:def 7;
consider k being Nat such that
A39: Jk . i = Jordan_block L,k by A37, Def3;
Jk . i <> {} by A37, FUNCT_1:def 15;
then len (Jk . i) in Seg (len (Jk . i)) by FINSEQ_1:5;
then [(len (Jk . i)),(len (Jk . i))] in [:(Seg (len (Jk . i))),(Seg (len (Jk . i))):] by ZFMISC_1:106;
then A40: [(len (Jk . i)),(len (Jk . i))] in Indices (Jk . i) by MATRIX_1:25;
then L = (Jk . i) * (len (Jk . i)),(len (Jk . i)) by A39, Def1
.= L1 by A38, A40, A36, Def1 ;
hence L1 is eigenvalue of F by A7, A8, 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
A41: ( j in dom Ji & i = (len Jk) + j ) ;
JJ . i = Ji . j by A41, FINSEQ_1:def 7;
then L1 is eigenvalue of FI by A36, A41, A28;
then consider w being Vector of (im ((F + ((- L) * (id V))) |^ m)) such that
A42: ( w <> 0. (im ((F + ((- L) * (id V))) |^ m)) & FI . w = L1 * w ) by A26, VECTSP11:def 2;
reconsider W = w as Vector of V by VECTSP_4:18;
A43: 0. (im ((F + ((- L) * (id V))) |^ m)) = 0. V by VECTSP_4:19;
L1 * W = FI . w by A42, VECTSP_4:22
.= F . W by FUNCT_1:72 ;
hence L1 is eigenvalue of F by A7, A42, A43, VECTSP11:def 2; :: thesis:

end;

A44: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A3);
let V be non trivial finite-dimensional VectSp of K; :: thesis:
let F be linear-transformation of V,V; :: thesis:
S₁[ dim V] by A44;
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: