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

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: ( 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 A5: 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
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: (J (+) (mlt ((len J) |-> a),(1. K,(Len J)))) . i = Jordan_block (L + a),n
A8: len (J . i) = n by A7, MATRIX_1:25;
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 FINSEQ_1:def 18;
then dom ((len J) |-> a) = dom J by FINSEQ_3:31;
then ((len J) |-> a) /. i = ((len J) |-> a) . i by A6, PARTFUN1:def 8
.= a by A6, A3, FINSEQ_2:71 ;
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: 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 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
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: 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 i in dom JM ; :: thesis: ex n being Nat st JM . i = Jordan_block (L + a),n
hence ex n being Nat st JM . i = Jordan_block (L + a),n by 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