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 that
A1: i in dom B1 and
A2: i <> len B1 ; :: thesis: Sum (lmlt ((Line ((Jordan_block (L,(len B1))),i)),B1)) = (L * (B1 /. i)) + (B1 /. (i + 1))
set N = len B1;
A3: dom B1 = Seg (len B1) by FINSEQ_1:def 3;
i <= len B1 by A1, FINSEQ_3:25;
then i < len B1 by A2, XXREAL_0:1;
then ( 1 <= i + 1 & i + 1 <= len B1 ) by NAT_1:11, NAT_1:13;
then A4: i + 1 in dom B1 by A3;
set ONE = 1. (K,(len B1));
A5: len (Line ((1. (K,(len B1))),(i + 1))) = width (1. (K,(len B1))) by CARD_1:def 7;
width (1. (K,(len B1))) = len B1 by MATRIX_0:24;
then A6: dom (Line ((1. (K,(len B1))),(i + 1))) = dom B1 by A5, FINSEQ_3:29;
( 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))) ) by CARD_1:def 7, MATRIXR1:16;
then dom (L * (Line ((1. (K,(len B1))),i))) = dom (Line ((1. (K,(len B1))),(i + 1))) by A5, FINSEQ_3:29;
then A7: dom (lmlt ((L * (Line ((1. (K,(len B1))),i))),B1)) = dom B1 by A6, MATRLIN:12;
dom (lmlt ((Line ((1. (K,(len B1))),(i + 1))),B1)) = dom B1 by A6, MATRLIN:12;
then A8: len (lmlt ((L * (Line ((1. (K,(len B1))),i))),B1)) = len (lmlt ((Line ((1. (K,(len B1))),(i + 1))),B1)) by A7, FINSEQ_3:29;
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, A3, 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 A8, 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 A4, MATRLIN2:16 ; :: thesis: verum