theorem Th7: :: MATRIXJ2:7

for i, n being Nat
for K being Field
for L being Element of K
for F being Element of n -tuples_on the carrier of K st i in Seg n holds
( ( i = 1 implies (Col ((Jordan_block (L,n)),i)) "*" F = L * (F /. i) ) & ( i <> 1 implies (Col ((Jordan_block (L,n)),i)) "*" F = (L * (F /. i)) + (F /. (i - 1)) ) )