let i be Nat; :: thesis: 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))
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 i in dom B1 & i <> len B1 holds
Sum (lmlt (Line (Jordan_block L,(len B1)),i),B1) = (L * (B1 /. i)) + (B1 /. (i + 1))
let L be Element of K; :: thesis: 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))
let V1 be finite-dimensional VectSp of K; :: thesis: 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))
let B1 be FinSequence of V1; :: thesis: ( i in dom B1 & i <> len B1 implies Sum (lmlt (Line (Jordan_block L,(len B1)),i),B1) = (L * (B1 /. i)) + (B1 /. (i + 1)) )
assume A1: ( i in dom B1 & i <> len B1 ) ; :: thesis: Sum (lmlt (Line (Jordan_block L,(len B1)),i),B1) = (L * (B1 /. i)) + (B1 /. (i + 1))
set N = len B1;
set ONE = 1. K,(len B1);
set J = Jordan_block L,(len B1);
A2: ( width (1. K,(len B1)) = len B1 & dom B1 = Seg (len B1) ) by FINSEQ_1:def 3, MATRIX_1:25;
i <= len B1 by A1, FINSEQ_3:27;
then i < len B1 by A1, XXREAL_0:1;
then ( 1 <= i + 1 & i + 1 <= len B1 ) by NAT_1:11, NAT_1:13;
then A3: i + 1 in dom B1 by A2;
( len (L * (Line (1. K,(len B1)),i)) = len (Line (1. K,(len B1)),i) & len (Line (1. K,(len B1)),i) = width (1. K,(len B1)) & len (Line (1. K,(len B1)),(i + 1)) = width (1. K,(len B1)) ) by FINSEQ_1:def 18, MATRIXR1:16;
then ( dom (L * (Line (1. K,(len B1)),i)) = dom (Line (1. K,(len B1)),(i + 1)) & dom (Line (1. K,(len B1)),(i + 1)) = dom B1 ) by A2, FINSEQ_3:31;
then ( dom (lmlt (L * (Line (1. K,(len B1)),i)),B1) = dom B1 & dom (lmlt (Line (1. K,(len B1)),(i + 1)),B1) = dom B1 ) by MATRLIN:16;
then A4: len (lmlt (L * (Line (1. K,(len B1)),i)),B1) = len (lmlt (Line (1. K,(len B1)),(i + 1)),B1) by FINSEQ_3:31;
thus Sum (lmlt (Line (Jordan_block L,(len B1)),i),B1) = Sum (lmlt ((L * (Line (1. K,(len B1)),i)) + (Line (1. K,(len B1)),(i + 1))),B1) by A1, A2, Th4
.= Sum ((lmlt (L * (Line (1. K,(len B1)),i)),B1) + (lmlt (Line (1. K,(len B1)),(i + 1)),B1)) by MATRLIN2:7
.= (Sum (lmlt (L * (Line (1. K,(len B1)),i)),B1)) + (Sum (lmlt (Line (1. K,(len B1)),(i + 1)),B1)) by A4, MATRLIN2:10
.= (L * (Sum (lmlt (Line (1. K,(len B1)),i),B1))) + (Sum (lmlt (Line (1. K,(len B1)),(i + 1)),B1)) by MATRLIN2:13
.= (L * (B1 /. i)) + (Sum (lmlt (Line (1. K,(len B1)),(i + 1)),B1)) by A1, MATRLIN2:16
.= (L * (B1 /. i)) + (B1 /. (i + 1)) by A3, MATRLIN2:16 ; :: thesis: verum