let n be Nat; :: thesis: for K being Field
for a, L being Element of K holds (Jordan_block (L,n)) + (a * (1. (K,n))) = Jordan_block ((L + a),n)
let K be Field; :: thesis: for a, L being Element of K holds (Jordan_block (L,n)) + (a * (1. (K,n))) = Jordan_block ((L + a),n)
let a, L 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 :: thesis: for i, j being Nat st [i,j] in Indices (Jordan_block ((L + a),n)) holds
(Jordan_block ((L + a),n)) * (i,j) = ((Jordan_block (L,n)) + (a * (1. (K,n)))) * (i,j)

A1: Indices (Jordan_block (L,n)) = Indices (Jordan_block ((L + a),n)) by MATRIX_0:26;
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_0:26;

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

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))
.= ((Jordan_block (L,n)) * (i,j)) + (a * ((1. (K,n)) * (i,j))) by A2, A1, A3, A4, MATRIX_1:def 3
.= ((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 4
.= ((Jordan_block (L,n)) * (i,j)) + (0. K) by A2, A1, A5, Def1
.= ((Jordan_block (L,n)) * (i,j)) + (a * (0. K))
.= ((Jordan_block (L,n)) * (i,j)) + (a * ((1. (K,n)) * (i,j))) by A2, A1, A3, A6, MATRIX_1:def 3
.= ((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 4
.= ((Jordan_block (L,n)) * (i,j)) + (0. K) by A2, A1, A7, Def1
.= ((Jordan_block (L,n)) * (i,j)) + (a * (0. K))
.= ((Jordan_block (L,n)) * (i,j)) + (a * ((1. (K,n)) * (i,j))) by A2, A1, A3, A7, MATRIX_1:def 3
.= ((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_0:27; :: thesis: verum