let K be Field; :: thesis: for a, L 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 a, L 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_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: 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