let n be Nat; :: thesis: for K being Field
for L, a being Element of K holds (Jordan_block L,n) + (a * (1. K,n)) = Jordan_block (L + a),n
let K be Field; :: thesis: for L, a being Element of K holds (Jordan_block L,n) + (a * (1. K,n)) = Jordan_block (L + a),n
let L, a be Element of K; :: thesis: (Jordan_block L,n) + (a * (1. K,n)) = Jordan_block (L + a),n
set J = Jordan_block L,n;
set Ja = Jordan_block (L + a),n;
set ONE = 1. K,n;

now

A1: Indices (Jordan_block L,n) = Indices (Jordan_block (L + a),n) by MATRIX_1:27;
let i, j be Nat; :: thesis: ( [i,j] in Indices (Jordan_block (L + a),n) implies (Jordan_block (L + a),n) * i,j = ((Jordan_block L,n) + (a * (1. K,n))) * i,j )
assume A2: [i,j] in Indices (Jordan_block (L + a),n) ; :: thesis: (Jordan_block (L + a),n) * i,j = ((Jordan_block L,n) + (a * (1. K,n))) * i,j
A3: Indices (Jordan_block L,n) = Indices (1. K,n) by MATRIX_1:27;

now

per cases ( i = j or i + 1 = j or ( i <> j & i + 1 <> j ) ) ;

suppose A4: i = j ; :: thesis: (Jordan_block (L + a),n) * i,j = ((Jordan_block L,n) + (a * (1. K,n))) * i,j

hence (Jordan_block (L + a),n) * i,j = L + a by A2, Def1
.= ((Jordan_block L,n) * i,j) + a by A2, A1, A4, Def1
.= ((Jordan_block L,n) * i,j) + (a * (1_ K)) by VECTSP_1:def 16
.= ((Jordan_block L,n) * i,j) + (a * ((1. K,n) * i,j)) by A2, A1, A3, A4, MATRIX_1:def 12
.= ((Jordan_block L,n) * i,j) + ((a * (1. K,n)) * i,j) by A2, A1, A3, MATRIX_3:def 5
.= ((Jordan_block L,n) + (a * (1. K,n))) * i,j by A2, A1, MATRIX_3:def 3 ;
:: thesis: verum

end;

suppose A5: i + 1 = j ; :: thesis: (Jordan_block (L + a),n) * i,j = ((Jordan_block L,n) + (a * (1. K,n))) * i,j

then A6: i <> j ;
thus (Jordan_block (L + a),n) * i,j = 1_ K by A2, A5, Def1
.= (1_ K) + (0. K) by RLVECT_1:def 7
.= ((Jordan_block L,n) * i,j) + (0. K) by A2, A1, A5, Def1
.= ((Jordan_block L,n) * i,j) + (a * (0. K)) by VECTSP_1:36
.= ((Jordan_block L,n) * i,j) + (a * ((1. K,n) * i,j)) by A2, A1, A3, A6, MATRIX_1:def 12
.= ((Jordan_block L,n) * i,j) + ((a * (1. K,n)) * i,j) by A2, A1, A3, MATRIX_3:def 5
.= ((Jordan_block L,n) + (a * (1. K,n))) * i,j by A2, A1, MATRIX_3:def 3 ; :: thesis: verum

end;

suppose A7: ( i <> j & i + 1 <> j ) ; :: thesis: (Jordan_block (L + a),n) * i,j = ((Jordan_block L,n) + (a * (1. K,n))) * i,j

hence (Jordan_block (L + a),n) * i,j = 0. K by A2, Def1
.= (0. K) + (0. K) by RLVECT_1:def 7
.= ((Jordan_block L,n) * i,j) + (0. K) by A2, A1, A7, Def1
.= ((Jordan_block L,n) * i,j) + (a * (0. K)) by VECTSP_1:36
.= ((Jordan_block L,n) * i,j) + (a * ((1. K,n) * i,j)) by A2, A1, A3, A7, MATRIX_1:def 12
.= ((Jordan_block L,n) * i,j) + ((a * (1. K,n)) * i,j) by A2, A1, A3, MATRIX_3:def 5
.= ((Jordan_block L,n) + (a * (1. K,n))) * i,j by A2, A1, MATRIX_3:def 3 ;
:: thesis: verum

end;

end;

end;

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

end;

hence (Jordan_block L,n) + (a * (1. K,n)) = Jordan_block (L + a),n by MATRIX_1:28; :: thesis: verum