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