let K be Field; :: thesis:
let a, L be Element of K; :: thesis:
let J be FinSequence_of_Jordan_block of L,K; :: thesis:
set M = mlt (((len J) |-> a),(1. (K,(Len J))));
A1: for i being Nat st i in dom (J (+) (mlt (((len J) |-> a),(1. (K,(Len J)))))) holds
ex n being Nat st (J (+) (mlt (((len J) |-> a),(1. (K,(Len J)))))) . i = Jordan_block ((L + a),n)

A2: dom (mlt (((len J) |-> a),(1. (K,(Len J))))) = dom (1. (K,(Len J))) by MATRIXJ1:def 9;
A3: dom J = Seg (len J) by FINSEQ_1:def 3;
A4: dom (1. (K,(Len J))) = dom (Len J) by MATRIXJ1:def 8;
let i be Nat; :: thesis:
assume A5: i in dom (J (+) (mlt (((len J) |-> a),(1. (K,(Len J)))))) ; :: thesis:
A6: i in dom J by A5, MATRIXJ1:def 10;
then consider n being Nat such that
A7: J . i = Jordan_block (L,n) by Def3;
take n ; :: thesis:
A8: len (J . i) = n by A7, MATRIX_0:24;
A9: dom (Len J) = dom J by MATRIXJ1:def 3;
then A10: (Len J) . i = len (J . i) by A6, MATRIXJ1:def 3;
len ((len J) |-> a) = len J by CARD_1:def 7;
then dom ((len J) |-> a) = dom J by FINSEQ_3:29;
then ((len J) |-> a) /. i = ((len J) |-> a) . i by A6, PARTFUN1:def 6
.= a by A6, A3, FINSEQ_2:57 ;
then (mlt (((len J) |-> a),(1. (K,(Len J))))) . i = a * ((1. (K,(Len J))) . i) by A6, A2, A4, A9, MATRIXJ1:def 9
.= a * (1. (K,n)) by A6, A4, A9, A10, A8, MATRIXJ1:def 8 ;
hence (J (+) (mlt (((len J) |-> a),(1. (K,(Len J)))))) . i = (Jordan_block (L,n)) + (a * (1. (K,n))) by A5, A7, MATRIXJ1:def 10
.= Jordan_block ((L + a),n) by Th9 ;
:: thesis:

end;

let i be Nat; :: according to MATRIXJ2:def 2 :: thesis:
assume i in dom (J (+) (mlt (((len J) |-> a),(1. (K,(Len J)))))) ; :: thesis:
then ex n being Nat st (J (+) (mlt (((len J) |-> a),(1. (K,(Len J)))))) . i = Jordan_block ((L + a),n) by A1;
hence ex L being Element of K ex n being Nat st (J (+) (mlt (((len J) |-> a),(1. (K,(Len J)))))) . i = Jordan_block (L,n) ; :: thesis:

end;

end;