let n be Nat; :: thesis: for K being Field
for L being Element of K
for V being VectSp of K
for F being linear-transformation of V,V
for V1 being finite-dimensional Subspace of V
for F1 being linear-transformation of V1,V1 st V1 = ker ((F + ((- L) * (id V))) |^ n) & F | V1 = F1 holds
ex J being non-empty FinSequence_of_Jordan_block of L,K ex b1 being OrdBasis of V1 st AutMt F1,b1,b1 = block_diagonal J,(0. K)
let K be Field; :: thesis: for L being Element of K
for V being VectSp of K
for F being linear-transformation of V,V
for V1 being finite-dimensional Subspace of V
for F1 being linear-transformation of V1,V1 st V1 = ker ((F + ((- L) * (id V))) |^ n) & F | V1 = F1 holds
ex J being non-empty FinSequence_of_Jordan_block of L,K ex b1 being OrdBasis of V1 st AutMt F1,b1,b1 = block_diagonal J,(0. K)
let L be Element of K; :: thesis: for V being VectSp of K
for F being linear-transformation of V,V
for V1 being finite-dimensional Subspace of V
for F1 being linear-transformation of V1,V1 st V1 = ker ((F + ((- L) * (id V))) |^ n) & F | V1 = F1 holds
ex J being non-empty FinSequence_of_Jordan_block of L,K ex b1 being OrdBasis of V1 st AutMt F1,b1,b1 = block_diagonal J,(0. K)
let V be VectSp of K; :: thesis: for F being linear-transformation of V,V
for V1 being finite-dimensional Subspace of V
for F1 being linear-transformation of V1,V1 st V1 = ker ((F + ((- L) * (id V))) |^ n) & F | V1 = F1 holds
ex J being non-empty FinSequence_of_Jordan_block of L,K ex b1 being OrdBasis of V1 st AutMt F1,b1,b1 = block_diagonal J,(0. K)
let F be linear-transformation of V,V; :: thesis: for V1 being finite-dimensional Subspace of V
for F1 being linear-transformation of V1,V1 st V1 = ker ((F + ((- L) * (id V))) |^ n) & F | V1 = F1 holds
ex J being non-empty FinSequence_of_Jordan_block of L,K ex b1 being OrdBasis of V1 st AutMt F1,b1,b1 = block_diagonal J,(0. K)
let V1 be finite-dimensional Subspace of V; :: thesis: for F1 being linear-transformation of V1,V1 st V1 = ker ((F + ((- L) * (id V))) |^ n) & F | V1 = F1 holds
ex J being non-empty FinSequence_of_Jordan_block of L,K ex b1 being OrdBasis of V1 st AutMt F1,b1,b1 = block_diagonal J,(0. K)
let F1 be linear-transformation of V1,V1; :: thesis: ( V1 = ker ((F + ((- L) * (id V))) |^ n) & F | V1 = F1 implies ex J being non-empty FinSequence_of_Jordan_block of L,K ex b1 being OrdBasis of V1 st AutMt F1,b1,b1 = block_diagonal J,(0. K) )
assume that
A1: V1 = ker ((F + ((- L) * (id V))) |^ n) and
A2: F | V1 = F1 ; :: thesis: ex J being non-empty FinSequence_of_Jordan_block of L,K ex b1 being OrdBasis of V1 st AutMt F1,b1,b1 = block_diagonal J,(0. K)
set FL = F + ((- L) * (id V));
reconsider FLV = (F + ((- L) * (id V))) | V1 as nilpotent linear-transformation of V1,V1 by A1, Th14;

A3: now

let x be set ; :: thesis: ( x in dom FLV implies FLV . x = (F1 + ((- L) * (id V1))) . x )
assume x in dom FLV ; :: thesis: FLV . x = (F1 + ((- L) * (id V1))) . x
then reconsider v1 = x as Vector of V1 by FUNCT_2:def 1;
reconsider v = v1 as Vector of V by VECTSP_4:18;
(id V) . v = v by FUNCT_1:35;
then A4: (- L) * ((id V) . v) = (- L) * ((id V1) . v1) by FUNCT_1:35, VECTSP_4:22;
A5: F . v1 = F1 . v1 by A2, FUNCT_1:72;
thus FLV . x = (F + ((- L) * (id V))) . v by FUNCT_1:72
.= (F . v) + (((- L) * (id V)) . v) by MATRLIN:def 5
.= (F . v) + ((- L) * ((id V) . v)) by MATRLIN:def 6
.= (F1 . v1) + ((- L) * ((id V1) . v1)) by A4, A5, VECTSP_4:21
.= (F1 . v1) + (((- L) * (id V1)) . v1) by MATRLIN:def 6
.= (F1 + ((- L) * (id V1))) . x by MATRLIN:def 5 ; :: thesis: verum

end;

dom FLV = the carrier of V1 by FUNCT_2:def 1
.= dom (F1 + ((- L) * (id V1))) by FUNCT_2:def 1 ;
then A6: FLV = F1 + ((- L) * (id V1)) by A3, FUNCT_1:9;
consider J being non-empty FinSequence_of_Jordan_block of 0. K,K, b1 being OrdBasis of V1 such that
A7: AutMt FLV,b1,b1 = block_diagonal J,(0. K) by Th29;
L + (0. K) = L by RLVECT_1:def 7;
then reconsider JM = J (+) (mlt ((len J) |-> L),(1. K,(Len J))) as FinSequence_of_Jordan_block of L,K by Th12;

now

let x be set ; :: thesis: ( x in dom JM implies not JM . x is empty )
assume A8: x in dom JM ; :: thesis: not JM . x is empty
reconsider i = x as Nat by A8;
A9: JM . i = (J . i) + ((mlt ((len J) |-> L),(1. K,(Len J))) . i) by A8, MATRIXJ1:def 10;
dom JM = dom J by MATRIXJ1:def 10;
then J . i <> {} by A8, FUNCT_1:def 15;
hence not JM . x is empty by A9, MATRIX_3:def 3; :: thesis: verum

end;

then reconsider JM = JM as non-empty FinSequence_of_Jordan_block of L,K by FUNCT_1:def 15;
take JM ; :: thesis: ex b1 being OrdBasis of V1 st AutMt F1,b1,b1 = block_diagonal JM,(0. K)
take b1 ; :: thesis: AutMt F1,b1,b1 = block_diagonal JM,(0. K)
set Aid = AutMt (id V1),b1,b1;
set AF1 = AutMt F1,b1,b1;

A10: now

A11: Indices (AutMt (id V1),b1,b1) = Indices (AutMt F1,b1,b1) by MATRIX_1:27;
let i, j be Nat; :: thesis: ( [i,j] in Indices (AutMt F1,b1,b1) implies (((AutMt F1,b1,b1) + ((- L) * (AutMt (id V1),b1,b1))) + (L * (AutMt (id V1),b1,b1))) * i,j = (AutMt F1,b1,b1) * i,j )
assume A12: [i,j] in Indices (AutMt F1,b1,b1) ; :: thesis: (((AutMt F1,b1,b1) + ((- L) * (AutMt (id V1),b1,b1))) + (L * (AutMt (id V1),b1,b1))) * i,j = (AutMt F1,b1,b1) * i,j
Indices ((AutMt F1,b1,b1) + ((- L) * (AutMt (id V1),b1,b1))) = Indices (AutMt F1,b1,b1) by MATRIX_1:27;
hence (((AutMt F1,b1,b1) + ((- L) * (AutMt (id V1),b1,b1))) + (L * (AutMt (id V1),b1,b1))) * i,j = (((AutMt F1,b1,b1) + ((- L) * (AutMt (id V1),b1,b1))) * i,j) + ((L * (AutMt (id V1),b1,b1)) * i,j) by A12, MATRIX_3:def 3
.= (((AutMt F1,b1,b1) * i,j) + (((- L) * (AutMt (id V1),b1,b1)) * i,j)) + ((L * (AutMt (id V1),b1,b1)) * i,j) by A12, MATRIX_3:def 3
.= ((AutMt F1,b1,b1) * i,j) + ((((- L) * (AutMt (id V1),b1,b1)) * i,j) + ((L * (AutMt (id V1),b1,b1)) * i,j)) by RLVECT_1:def 6
.= ((AutMt F1,b1,b1) * i,j) + (((- L) * ((AutMt (id V1),b1,b1) * i,j)) + ((L * (AutMt (id V1),b1,b1)) * i,j)) by A12, A11, MATRIX_3:def 5
.= ((AutMt F1,b1,b1) * i,j) + (((- L) * ((AutMt (id V1),b1,b1) * i,j)) + (L * ((AutMt (id V1),b1,b1) * i,j))) by A12, A11, MATRIX_3:def 5
.= ((AutMt F1,b1,b1) * i,j) + (((- L) + L) * ((AutMt (id V1),b1,b1) * i,j)) by VECTSP_1:def 12
.= ((AutMt F1,b1,b1) * i,j) + ((0. K) * ((AutMt (id V1),b1,b1) * i,j)) by VECTSP_1:63
.= ((AutMt F1,b1,b1) * i,j) + (0. K) by VECTSP_1:39
.= (AutMt F1,b1,b1) * i,j by RLVECT_1:def 7 ;
:: thesis: verum

end;

A13: Len (mlt ((len J) |-> L),(1. K,(Len J))) = Len (1. K,(Len J)) by MATRIXJ1:62
.= Len J by MATRIXJ1:56 ;
dom (Len J) = dom (1. K,(Len J)) by MATRIXJ1:def 8;
then A14: len (1. K,(Len J)) = len (Len J) by FINSEQ_3:31
.= len J by FINSEQ_1:def 18 ;
A15: Sum (Len J) = len (AutMt FLV,b1,b1) by A7, MATRIXJ1:def 5
.= len b1 by MATRIX_1:def 3 ;
A16: Width (mlt ((len J) |-> L),(1. K,(Len J))) = Width (1. K,(Len J)) by MATRIXJ1:62
.= Len J by MATRIXJ1:56
.= Width J by MATRIXJ1:46 ;
Mx2Tran (AutMt ((- L) * (id V1)),b1,b1),b1,b1 = (- L) * (id V1) by MATRLIN2:34
.= (- L) * (Mx2Tran (AutMt (id V1),b1,b1),b1,b1) by MATRLIN2:34
.= Mx2Tran ((- L) * (AutMt (id V1),b1,b1)),b1,b1 by MATRLIN2:38 ;
then AutMt ((- L) * (id V1)),b1,b1 = (- L) * (AutMt (id V1),b1,b1) by MATRLIN2:39;
then (AutMt FLV,b1,b1) + (L * (AutMt (id V1),b1,b1)) = ((AutMt F1,b1,b1) + ((- L) * (AutMt (id V1),b1,b1))) + (L * (AutMt (id V1),b1,b1)) by A6, MATRLIN:47
.= AutMt F1,b1,b1 by A10, MATRIX_1:28 ;
hence AutMt F1,b1,b1 = (block_diagonal J,(0. K)) + (L * (1. K,(Sum (Len J)))) by A7, A15, MATRLIN2:28
.= (block_diagonal J,(0. K)) + (L * (block_diagonal (1. K,(Len J)),(0. K))) by MATRIXJ1:61
.= (block_diagonal J,(0. K)) + (block_diagonal (mlt ((len J) |-> L),(1. K,(Len J))),(L * (0. K))) by A14, MATRIXJ1:65
.= (block_diagonal J,(0. K)) + (block_diagonal (mlt ((len J) |-> L),(1. K,(Len J))),(0. K)) by VECTSP_1:39
.= block_diagonal JM,((0. K) + (0. K)) by A13, A16, MATRIXJ1:72
.= block_diagonal JM,(0. K) by RLVECT_1:def 7 ;
:: thesis: verum