theorem Th9: :: MATRIXJ2:9
for n being Nat
for K being Field
for a, L being Element of K holds (Jordan_block (L,n)) + (a * (1. (K,n))) = Jordan_block ((L + a),n)