let K be Field; :: thesis: 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))
let L be Element of K; :: thesis: 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))
let V1 be finite-dimensional VectSp of K; :: thesis: 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))
let B1 be FinSequence of V1; :: thesis: ( len B1 in dom B1 implies Sum (lmlt (Line (Jordan_block L,(len B1)),(len B1)),B1) = L * (B1 /. (len B1)) )
set N = len B1;
assume A1: len B1 in dom B1 ; :: thesis: Sum (lmlt (Line (Jordan_block L,(len B1)),(len B1)),B1) = L * (B1 /. (len B1))
set J = Jordan_block L,(len B1);
set ONE = 1. K,(len B1);
thus Sum (lmlt (Line (Jordan_block L,(len B1)),(len B1)),B1) = Sum (lmlt (L * (Line (1. K,(len B1)),(len B1))),B1) by Th5
.= L * (Sum (lmlt (Line (1. K,(len B1)),(len B1)),B1)) by MATRLIN2:13
.= L * (B1 /. (len B1)) by A1, MATRLIN2:16 ; :: thesis: verum