let K be Field; :: thesis: for L, a being Element of K
for J being FinSequence_of_Jordan_block of L,K holds J (+) (mlt ((len J) |-> a),(1. K,(Len J))) is FinSequence_of_Jordan_block of L + a,K
let L, a be Element of K; :: thesis: for J being FinSequence_of_Jordan_block of L,K holds J (+) (mlt ((len J) |-> a),(1. K,(Len J))) is FinSequence_of_Jordan_block of L + a,K
let J be FinSequence_of_Jordan_block of L,K; :: thesis: J (+) (mlt ((len J) |-> a),(1. K,(Len J))) is FinSequence_of_Jordan_block of L + a,K
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

proof

let i be Nat; :: thesis: ( i in dom (J (+) (mlt ((len J) |-> a),(1. K,(Len J)))) implies ex n being Nat st (J (+) (mlt ((len J) |-> a),(1. K,(Len J)))) . i = Jordan_block (L + a),n )
assume A2: i in dom (J (+) (mlt ((len J) |-> a),(1. K,(Len J)))) ; :: thesis: ex n being Nat st (J (+) (mlt ((len J) |-> a),(1. K,(Len J)))) . i = Jordan_block (L + a),n
A3: ( i in dom J & dom J = Seg (len J) ) by A2, FINSEQ_1:def 3, MATRIXJ1:def 10;
then consider n being Nat such that
A4: J . i = Jordan_block L,n by Def3;
take n ; :: thesis: (J (+) (mlt ((len J) |-> a),(1. K,(Len J)))) . i = Jordan_block (L + a),n
len ((len J) |-> a) = len J by FINSEQ_1:def 18;
then dom ((len J) |-> a) = dom J by FINSEQ_3:31;
then A5: ((len J) |-> a) /. i = ((len J) |-> a) . i by A3, PARTFUN1:def 8
.= a by A3, FINSEQ_2:71 ;
A6: dom (mlt ((len J) |-> a),(1. K,(Len J))) = dom (1. K,(Len J)) by MATRIXJ1:def 9;
A7: dom (1. K,(Len J)) = dom (Len J) by MATRIXJ1:def 8;
A8: dom (Len J) = dom J by MATRIXJ1:def 3;
then A9: ( (Len J) . i = len (J . i) & len (J . i) = n ) by A4, A3, MATRIXJ1:def 3, MATRIX_1:25;
(mlt ((len J) |-> a),(1. K,(Len J))) . i = a * ((1. K,(Len J)) . i) by A3, A6, A5, A7, A8, MATRIXJ1:def 9
.= a * (1. K,n) by A9, A3, A7, A8, MATRIXJ1:def 8 ;
hence (J (+) (mlt ((len J) |-> a),(1. K,(Len J)))) . i = (Jordan_block L,n) + (a * (1. K,n)) by A4, A2, MATRIXJ1:def 10
.= Jordan_block (L + a),n by Th9 ;
:: thesis: verum

end;

J (+) (mlt ((len J) |-> a),(1. K,(Len J))) is Jordan-block-yielding

proof

let i be Nat; :: according to MATRIXJ2:def 2 :: thesis: ( i in dom (J (+) (mlt ((len J) |-> a),(1. K,(Len J)))) implies 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 )
assume A10: i in dom (J (+) (mlt ((len J) |-> a),(1. K,(Len J)))) ; :: thesis: 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
ex n being Nat st (J (+) (mlt ((len J) |-> a),(1. K,(Len J)))) . i = Jordan_block (L + a),n by A10, 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: verum

end;

then reconsider JM = J (+) (mlt ((len J) |-> a),(1. K,(Len J))) as FinSequence_of_Jordan_block of K ;
JM is FinSequence_of_Jordan_block of L + a,K

proof

let i be Nat; :: according to MATRIXJ2:def 3 :: thesis: ( i in dom JM implies ex n being Nat st JM . i = Jordan_block (L + a),n )
assume A11: i in dom JM ; :: thesis: ex n being Nat st JM . i = Jordan_block (L + a),n
thus ex n being Nat st JM . i = Jordan_block (L + a),n by A11, A1; :: thesis: verum

end;

hence J (+) (mlt ((len J) |-> a),(1. K,(Len J))) is FinSequence_of_Jordan_block of L + a,K ; :: thesis: verum