theorem Th22: :: MATRIXJ2:22

for i being Nat
for K being Field
for L being Element of K
for V1 being finite-dimensional VectSp of K
for B1 being FinSequence of V1 st i in dom B1 & i <> len B1 holds
Sum (lmlt ((Line ((Jordan_block (L,(len B1))),i)),B1)) = (L * (B1 /. i)) + (B1 /. (i + 1))