theorem Th6: :: MATRIXJ2:6

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 <> n implies (Line ((Jordan_block (L,n)),i)) "*" F = (L * (F /. i)) + (F /. (i + 1)) ) & ( i = n implies (Line ((Jordan_block (L,n)),i)) "*" F = L * (F /. i) ) )