let n be Nat; :: thesis:
let K be Field; :: thesis:
let L be Element of K; :: thesis:
assume A1: L <> 0. K ; :: thesis:
reconsider N = n as Element of NAT by ORDINAL1:def 13;
defpred S₁[ Nat, Nat, set ] means ( ( $1 > $2 implies $3 = 0. K ) & ( $1 <= $2 implies $3 = - ((power K) . (- (L " )),(($2 -' $1) + 1)) ) );
A2: for i, j being Nat st [i,j] in [:(Seg N),(Seg N):] holds
for x1, x2 being Element of K st S₁[i,j,x1] & S₁[i,j,x2] holds
x1 = x2 ;
A3: for i, j being Nat st [i,j] in [:(Seg N),(Seg N):] holds
ex x being Element of K st S₁[i,j,x]

proof

let i, j be Nat; :: thesis:
assume [i,j] in [:(Seg N),(Seg N):] ; :: thesis:

per cases ;

suppose A4: i > j ; :: thesis:

take 0. K ; :: thesis:
thus S₁[i,j, 0. K] by A4; :: thesis:

end;

suppose A5: i <= j ; :: thesis:

take P = - ((power K) . (- (L " )),((j -' i) + 1)); :: thesis:
thus S₁[i,j,P] by A5; :: thesis:

end;

consider M being Matrix of N,K such that
A6: for i, j being Nat st [i,j] in Indices M holds
S₁[i,j,M * i,j] from MATRIX_1:sch 2(A2, A3);
reconsider M = M as Matrix of n,K ;
take M ; :: thesis:
set J = Jordan_block L,n;
set ONE = 1. K,n;
set JM = (Jordan_block L,n) * M;
set MJ = M * (Jordan_block L,n);
A7: ( Jordan_block L,n is invertible & Indices M = Indices (Jordan_block L,n) & Indices (Jordan_block L,n) = Indices (1. K,n) & Indices ((Jordan_block L,n) * M) = Indices (1. K,n) & Indices (M * (Jordan_block L,n)) = Indices (1. K,n) & Indices (1. K,n) = [:(Seg n),(Seg n):] ) by A1, Th3, MATRIX_1:25, MATRIX_1:27;
A8: ( len M = n & width M = n & len (Jordan_block L,n) = n & width (Jordan_block L,n) = n ) by MATRIX_1:25;

now

let i, j be Nat; :: thesis:
assume A9: [i,j] in Indices (1. K,n) ; :: thesis:
set C = Col M,j;
set i1 = i + 1;
A10: ( i in Seg n & j in Seg n & dom M = Seg n & dom (Col M,j) = Seg n ) by A7, A8, A9, FINSEQ_1:def 3, FINSEQ_2:144, ZFMISC_1:106;
then A11: ( (Col M,j) /. i = (Col M,j) . i & (Col M,j) . i = M * i,j ) by MATRIX_1:def 9, PARTFUN1:def 8;
A12: ((Jordan_block L,n) * M) * i,j = (Line (Jordan_block L,n),i) "*" (Col M,j) by A7, A8, A9, MATRIX_3:def 4;

now

per cases ;

suppose A13: i = n ; :: thesis:

then A14: ((Jordan_block L,n) * M) * i,j = L * (M * i,j) by A12, A8, A10, Th6, A11;

now

per cases ;

suppose A15: i > j ; :: thesis:

hence ((Jordan_block L,n) * M) * i,j = L * (0. K) by A7, A9, A14, A6
.= 0. K by VECTSP_1:36
.= (1. K,n) * i,j by A9, A15, MATRIX_1:def 12 ;
:: thesis:

end;

suppose A16: i <= j ; :: thesis:

j <= n by A10, FINSEQ_1:3;
then A17: j = n by A13, A16, XXREAL_0:1;
hence ((Jordan_block L,n) * M) * i,j = L * (- ((power K) . (- (L " )),((n -' n) + 1))) by A7, A9, A14, A13, A6
.= L * (- ((power K) . (- (L " )),(0 + 1))) by XREAL_1:234
.= L * (- (- (L " ))) by GROUP_1:98
.= L * (L " ) by RLVECT_1:30
.= 1_ K by A1, VECTSP_1:def 22
.= (1. K,n) * i,j by A9, A13, A17, MATRIX_1:def 12 ;
:: thesis:

end;

hence ((Jordan_block L,n) * M) * i,j = (1. K,n) * i,j ; :: thesis:

end;

suppose A18: i <> n ; :: thesis:

i <= n by A10, FINSEQ_1:3;
then i < n by A18, XXREAL_0:1;
then ( 1 <= i + 1 & i + 1 <= n ) by NAT_1:11, NAT_1:13;
then i + 1 in Seg n ;
then A19: ( (Col M,j) /. (i + 1) = (Col M,j) . (i + 1) & (Col M,j) . (i + 1) = M * (i + 1),j & [(i + 1),j] in Indices M ) by A7, A10, MATRIX_1:def 9, PARTFUN1:def 8, ZFMISC_1:106;
then A20: ((Jordan_block L,n) * M) * i,j = (L * (M * i,j)) + (M * (i + 1),j) by A12, A8, A10, Th6, A11, A18;

now

per cases by XXREAL_0:1;

suppose A21: i > j ; :: thesis:

then i + 1 > j by NAT_1:13;
hence ((Jordan_block L,n) * M) * i,j = (L * (M * i,j)) + (0. K) by A19, A20, A6
.= L * (M * i,j) by RLVECT_1:def 7
.= L * (0. K) by A9, A7, A6, A21
.= 0. K by VECTSP_1:36
.= (1. K,n) * i,j by A9, A21, MATRIX_1:def 12 ;
:: thesis:

end;

suppose A22: i = j ; :: thesis:

then i + 1 > j by NAT_1:13;
hence ((Jordan_block L,n) * M) * i,j = (L * (M * i,j)) + (0. K) by A19, A20, A6
.= L * (M * i,i) by A22, RLVECT_1:def 7
.= L * (- ((power K) . (- (L " )),((i -' i) + 1))) by A9, A7, A6, A22
.= L * (- ((power K) . (- (L " )),(0 + 1))) by XREAL_1:234
.= L * (- (- (L " ))) by GROUP_1:98
.= L * (L " ) by RLVECT_1:30
.= 1_ K by A1, VECTSP_1:def 22
.= (1. K,n) * i,j by A9, A22, MATRIX_1:def 12 ;
:: thesis:

end;

suppose A23: i < j ; :: thesis:

then A24: i + 1 <= j by NAT_1:13;
then A25: ( j -' (i + 1) = j - (i + 1) & j -' i = j - i ) by A23, XREAL_1:235;
set P = (power K) . (- (L " )),((j -' (i + 1)) + 1);
thus ((Jordan_block L,n) * M) * i,j = (L * (M * i,j)) + (- ((power K) . (- (L " )),((j -' (i + 1)) + 1))) by A19, A20, A6, A24
.= (L * (- ((power K) . (- (L " )),((j -' i) + 1)))) + (- ((power K) . (- (L " )),((j -' (i + 1)) + 1))) by A9, A7, A6, A23
.= (L * (- ((- (L " )) * ((power K) . (- (L " )),((j -' (i + 1)) + 1))))) + (- ((power K) . (- (L " )),((j -' (i + 1)) + 1))) by A25, GROUP_1:def 8
.= (L * ((- (- (L " ))) * ((power K) . (- (L " )),((j -' (i + 1)) + 1)))) + (- ((power K) . (- (L " )),((j -' (i + 1)) + 1))) by VECTSP_1:41
.= (L * ((L " ) * ((power K) . (- (L " )),((j -' (i + 1)) + 1)))) + (- ((power K) . (- (L " )),((j -' (i + 1)) + 1))) by RLVECT_1:30
.= ((L * (L " )) * ((power K) . (- (L " )),((j -' (i + 1)) + 1))) + (- ((power K) . (- (L " )),((j -' (i + 1)) + 1))) by GROUP_1:def 4
.= ((1_ K) * ((power K) . (- (L " )),((j -' (i + 1)) + 1))) + (- ((power K) . (- (L " )),((j -' (i + 1)) + 1))) by A1, VECTSP_1:def 22
.= ((power K) . (- (L " )),((j -' (i + 1)) + 1)) + (- ((power K) . (- (L " )),((j -' (i + 1)) + 1))) by VECTSP_1:def 16
.= 0. K by RLVECT_1:def 11
.= (1. K,n) * i,j by A9, A23, MATRIX_1:def 12 ; :: thesis:

end;

hence (1. K,n) * i,j = ((Jordan_block L,n) * M) * i,j ; :: thesis:

end;

hence (1. K,n) * i,j = ((Jordan_block L,n) * M) * i,j ; :: thesis:

end;

then A26: 1. K,n = (Jordan_block L,n) * M by MATRIX_1:28;

now

let i, j be Nat; :: thesis:
assume A27: [i,j] in Indices (1. K,n) ; :: thesis:
set LL = Line M,i;
A28: ( i in Seg n & j in Seg n & dom (Line M,i) = Seg n ) by A7, A8, A27, FINSEQ_2:144, ZFMISC_1:106;
then A29: ( (Line M,i) /. j = (Line M,i) . j & (Line M,i) . j = M * i,j ) by A8, MATRIX_1:def 8, PARTFUN1:def 8;
A30: (M * (Jordan_block L,n)) * i,j = (Line M,i) "*" (Col (Jordan_block L,n),j) by A7, A8, A27, MATRIX_3:def 4
.= (Col (Jordan_block L,n),j) "*" (Line M,i) by FVSUM_1:115 ;

now

per cases ;

suppose A31: j = 1 ; :: thesis:

then A32: (M * (Jordan_block L,n)) * i,j = L * (M * i,j) by A8, A28, A29, A30, Th7;

now

per cases ;

suppose A33: i = j ; :: thesis:

hence (M * (Jordan_block L,n)) * i,j = L * (- ((power K) . (- (L " )),((i -' i) + 1))) by A7, A27, A6, A32
.= L * (- ((power K) . (- (L " )),(0 + 1))) by XREAL_1:234
.= L * (- (- (L " ))) by GROUP_1:98
.= L * (L " ) by RLVECT_1:30
.= 1_ K by A1, VECTSP_1:def 22
.= (1. K,n) * i,j by A27, A33, MATRIX_1:def 12 ;
:: thesis:

end;

suppose A34: i <> j ; :: thesis:

1 <= i by A28, FINSEQ_1:3;
then j < i by A31, A34, XXREAL_0:1;
hence (M * (Jordan_block L,n)) * i,j = L * (0. K) by A7, A27, A6, A32
.= 0. K by VECTSP_1:36
.= (1. K,n) * i,j by A27, A34, MATRIX_1:def 12 ;
:: thesis:

end;

hence (1. K,n) * i,j = (M * (Jordan_block L,n)) * i,j ; :: thesis:

end;

suppose A35: j <> 1 ; :: thesis:

A36: j >= 1 by A28, FINSEQ_1:3;
then reconsider j1 = j - 1 as Element of NAT by NAT_1:21;
j1 + 1 > 0 + 1 by A35, A36, XXREAL_0:1;
then ( j1 > 0 & j1 <= j1 + 1 & j <= n ) by A28, FINSEQ_1:3, NAT_1:11;
then ( n >= j1 & j1 >= 1 ) by NAT_1:14, XXREAL_0:2;
then j1 in Seg n ;
then A37: ( (Line M,i) /. j1 = (Line M,i) . j1 & (Line M,i) . j1 = M * i,j1 & [i,j1] in Indices (1. K,n) ) by A7, A8, A28, MATRIX_1:def 8, PARTFUN1:def 8, ZFMISC_1:106;
then A38: (M * (Jordan_block L,n)) * i,j = (L * (M * i,j)) + (M * i,j1) by A8, A28, A29, A35, A30, Th7;

now

per cases by XXREAL_0:1;

suppose A39: i < j1 + 1 ; :: thesis:

then A40: i <= j1 by NAT_1:13;
then A41: ( j1 -' i = j1 - i & j -' i = j - i ) by A39, XREAL_1:235;
set P = (power K) . (- (L " )),((j1 -' i) + 1);
thus (M * (Jordan_block L,n)) * i,j = (L * (M * i,j)) + (- ((power K) . (- (L " )),((j1 -' i) + 1))) by A7, A6, A37, A38, A40
.= (L * (- ((power K) . (- (L " )),((j -' i) + 1)))) + (- ((power K) . (- (L " )),((j1 -' i) + 1))) by A7, A6, A27, A39
.= (L * (- ((- (L " )) * ((power K) . (- (L " )),((j1 -' i) + 1))))) + (- ((power K) . (- (L " )),((j1 -' i) + 1))) by A41, GROUP_1:def 8
.= (L * ((- (- (L " ))) * ((power K) . (- (L " )),((j1 -' i) + 1)))) + (- ((power K) . (- (L " )),((j1 -' i) + 1))) by VECTSP_1:41
.= (L * ((L " ) * ((power K) . (- (L " )),((j1 -' i) + 1)))) + (- ((power K) . (- (L " )),((j1 -' i) + 1))) by RLVECT_1:30
.= ((L * (L " )) * ((power K) . (- (L " )),((j1 -' i) + 1))) + (- ((power K) . (- (L " )),((j1 -' i) + 1))) by GROUP_1:def 4
.= ((1_ K) * ((power K) . (- (L " )),((j1 -' i) + 1))) + (- ((power K) . (- (L " )),((j1 -' i) + 1))) by A1, VECTSP_1:def 22
.= ((power K) . (- (L " )),((j1 -' i) + 1)) + (- ((power K) . (- (L " )),((j1 -' i) + 1))) by VECTSP_1:def 16
.= 0. K by RLVECT_1:def 11
.= (1. K,n) * i,j by A27, A39, MATRIX_1:def 12 ; :: thesis:

end;

suppose A42: i = j1 + 1 ; :: thesis:

then i > j1 by NAT_1:13;
hence (M * (Jordan_block L,n)) * i,j = (L * (M * i,j)) + (0. K) by A7, A6, A37, A38
.= L * (M * i,j) by RLVECT_1:def 7
.= L * (- ((power K) . (- (L " )),((i -' i) + 1))) by A7, A42, A27, A6
.= L * (- ((power K) . (- (L " )),(0 + 1))) by XREAL_1:234
.= L * (- (- (L " ))) by GROUP_1:98
.= L * (L " ) by RLVECT_1:30
.= 1_ K by A1, VECTSP_1:def 22
.= (1. K,n) * i,j by A27, A42, MATRIX_1:def 12 ;
:: thesis:

end;

suppose A43: i > j1 + 1 ; :: thesis:

then i > j1 by NAT_1:13;
hence (M * (Jordan_block L,n)) * i,j = (L * (M * i,j)) + (0. K) by A7, A6, A37, A38
.= L * (M * i,j) by RLVECT_1:def 7
.= L * (0. K) by A7, A43, A27, A6
.= 0. K by VECTSP_1:36
.= (1. K,n) * i,j by A27, A43, MATRIX_1:def 12 ;
:: thesis:

end;

hence (M * (Jordan_block L,n)) * i,j = (1. K,n) * i,j ; :: thesis:

end;

hence (1. K,n) * i,j = (M * (Jordan_block L,n)) * i,j ; :: thesis:

end;

then 1. K,n = M * (Jordan_block L,n) by MATRIX_1:28;
then M is_reverse_of Jordan_block L,n by A26, MATRIX_6:def 2;
hence ( (Jordan_block L,n) ~ = M & ( for i, j being Nat st [i,j] in Indices M holds
( ( i > j implies M * i,j = 0. K ) & ( i <= j implies M * i,j = - ((power K) . (- (L " )),((j -' i) + 1)) ) ) ) ) by A6, A7, MATRIX_6:def 4; :: thesis: