theorem Th4: :: MATRIXJ2:4

for i, n being Nat
for K being Field
for L being Element of K st i in Seg n & i <> n holds
Line ((Jordan_block (L,n)),i) = (L * (Line ((1. (K,n)),i))) + (Line ((1. (K,n)),(i + 1)))