let K be Field; :: thesis: for L being Element of
for V1 being finite-dimensional VectSp of finite-dimensional
for B1 being FinSequence of 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 ; :: thesis: for V1 being finite-dimensional VectSp of finite-dimensional
for B1 being FinSequence of 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 finite-dimensional ; :: thesis: for B1 being FinSequence of 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 ; :: 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