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 len B1 in dom B1 holds
Sum (lmlt ((Line ((Jordan_block (L,(len B1))),(len B1))),B1)) = L * (B1 /. (len B1))