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 :: thesis: for x being object st x in dom FLV holds
FLV . x = (F1 + ((- L) * (id V1))) . x

let x be object ; :: 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:10;
(id V) . v = v by FUNCT_1:18;
then A4: (- L) * ((id V) . v) = (- L) * ((id V1) . v1) by FUNCT_1:18, VECTSP_4:14;
A5: F . v1 = F1 . v1 by A2, FUNCT_1:49;
thus FLV . x = (F + ((- L) * (id V))) . v by FUNCT_1:49
.= (F . v) + (((- L) * (id V)) . v) by MATRLIN:def 3
.= (F . v) + ((- L) * ((id V) . v)) by MATRLIN:def 4
.= (F1 . v1) + ((- L) * ((id V1) . v1)) by A4, A5, VECTSP_4:13
.= (F1 . v1) + (((- L) * (id V1)) . v1) by MATRLIN:def 4
.= (F1 + ((- L) * (id V1))) . x by MATRLIN:def 3 ; :: 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;
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 4;
then reconsider JM = J (+) (mlt (((len J) |-> L),(1. (K,(Len J))))) as FinSequence_of_Jordan_block of L,K by Th12;

now :: thesis: for x being object st x in dom JM holds
not JM . x is empty

let x be object ; :: 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 9;
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 9;
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 :: thesis: for i, j being Nat st [i,j] in Indices (AutMt (F1,b1,b1)) holds
(((AutMt (F1,b1,b1)) + ((- L) * (AutMt ((id V1),b1,b1)))) + (L * (AutMt ((id V1),b1,b1)))) * (i,j) = (AutMt (F1,b1,b1)) * (i,j)

A11: Indices (AutMt ((id V1),b1,b1)) = Indices (AutMt (F1,b1,b1)) by MATRIX_0:26;
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_0:26;
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 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, 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 3
.= ((AutMt (F1,b1,b1)) * (i,j)) + ((0. K) * ((AutMt ((id V1),b1,b1)) * (i,j))) by VECTSP_1:16
.= ((AutMt (F1,b1,b1)) * (i,j)) + (0. K)
.= (AutMt (F1,b1,b1)) * (i,j) by RLVECT_1:def 4 ;
:: 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:29
.= len J by CARD_1:def 7 ;
A15: Sum (Len J) = len (AutMt (FLV,b1,b1)) by A7, MATRIXJ1:def 5
.= len b1 by MATRIX_0:def 2 ;
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:42
.= AutMt (F1,b1,b1) by A10, MATRIX_0:27 ;
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)))
.= block_diagonal (JM,((0. K) + (0. K))) by A13, A16, MATRIXJ1:72
.= block_diagonal (JM,(0. K)) by RLVECT_1:def 4 ;
:: thesis: verum