for K being Field
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