let i, n be Nat; :: thesis: for K being Field
for L being Element of K
for F being Element of n -tuples_on the carrier of K st i in Seg n holds
( ( i = 1 implies (Col ((Jordan_block (L,n)),i)) "*" F = L * (F /. i) ) & ( i <> 1 implies (Col ((Jordan_block (L,n)),i)) "*" F = (L * (F /. i)) + (F /. (i - 1)) ) )
let K be Field; :: thesis: for L being Element of K
for F being Element of n -tuples_on the carrier of K st i in Seg n holds
( ( i = 1 implies (Col ((Jordan_block (L,n)),i)) "*" F = L * (F /. i) ) & ( i <> 1 implies (Col ((Jordan_block (L,n)),i)) "*" F = (L * (F /. i)) + (F /. (i - 1)) ) )
let L be Element of K; :: thesis: for F being Element of n -tuples_on the carrier of K st i in Seg n holds
( ( i = 1 implies (Col ((Jordan_block (L,n)),i)) "*" F = L * (F /. i) ) & ( i <> 1 implies (Col ((Jordan_block (L,n)),i)) "*" F = (L * (F /. i)) + (F /. (i - 1)) ) )
set J = Jordan_block (L,n);
set Ci = Col ((Jordan_block (L,n)),i);
reconsider N = n as Element of NAT by ORDINAL1:def 12;
let F be Element of n -tuples_on the carrier of K; :: thesis: ( i in Seg n implies ( ( i = 1 implies (Col ((Jordan_block (L,n)),i)) "*" F = L * (F /. i) ) & ( i <> 1 implies (Col ((Jordan_block (L,n)),i)) "*" F = (L * (F /. i)) + (F /. (i - 1)) ) ) )
assume A1: i in Seg n ; :: thesis: ( ( i = 1 implies (Col ((Jordan_block (L,n)),i)) "*" F = L * (F /. i) ) & ( i <> 1 implies (Col ((Jordan_block (L,n)),i)) "*" F = (L * (F /. i)) + (F /. (i - 1)) ) )
A2: i >= 1 by A1, FINSEQ_1:1;
then reconsider i1 = i - 1 as Element of NAT by NAT_1:21;
A3: ( len (Jordan_block (L,n)) = n & dom (Jordan_block (L,n)) = Seg (len (Jordan_block (L,n))) ) by FINSEQ_1:def 3, MATRIX_0:24;
then A4: (Col ((Jordan_block (L,n)),i)) . i = (Jordan_block (L,n)) * (i,i) by A1, MATRIX_0:def 8;
A5: i1 + 1 >= i1 by NAT_1:11;
n >= i by A1, FINSEQ_1:1;
then A6: n >= i1 by A5, XXREAL_0:2;
A7: Indices (Jordan_block (L,n)) = [:(Seg n),(Seg n):] by MATRIX_0:24;
then A8: [i,i] in Indices (Jordan_block (L,n)) by A1, ZFMISC_1:87;
reconsider Ci = Col ((Jordan_block (L,n)),i), f = F as Element of N -tuples_on the carrier of K by MATRIX_0:24;
A9: dom f = Seg n by FINSEQ_2:124;
then A10: f . i = f /. i by A1, PARTFUN1:def 6;
A11: dom (mlt (Ci,f)) = Seg n by FINSEQ_2:124;
then A12: (mlt (Ci,f)) /. i = (mlt (Ci,f)) . i by A1, PARTFUN1:def 6
.= ((Jordan_block (L,n)) * (i,i)) * (f /. i) by A1, A4, A10, FVSUM_1:61
.= L * (f /. i) by A8, Def1 ;
thus ( i = 1 implies (Col ((Jordan_block (L,n)),i)) "*" F = L * (F /. i) ) :: thesis: ( i <> 1 implies (Col ((Jordan_block (L,n)),i)) "*" F = (L * (F /. i)) + (F /. (i - 1)) )

proof

A13: ( (Col ((Jordan_block (L,n)),i)) . i = (Jordan_block (L,n)) * (i,i) & f . i = f /. i ) by A1, A3, A9, MATRIX_0:def 8, PARTFUN1:def 6;
A14: [i,i] in Indices (Jordan_block (L,n)) by A1, A7, ZFMISC_1:87;
assume A15: i = 1 ; :: thesis: (Col ((Jordan_block (L,n)),i)) "*" F = L * (F /. i)

now :: thesis: for j being Nat st j in Seg n & j <> i holds
(mlt ((Col ((Jordan_block (L,n)),i)),f)) . j = 0. K

let j be Nat; :: thesis: ( j in Seg n & j <> i implies (mlt ((Col ((Jordan_block (L,n)),i)),f)) . j = 0. K )
assume that
A16: j in Seg n and
A17: j <> i ; :: thesis: (mlt ((Col ((Jordan_block (L,n)),i)),f)) . j = 0. K
A18: f . j = f /. j by A9, A16, PARTFUN1:def 6;
1 <= j by A16, FINSEQ_1:1;
then A19: i < j + 1 by A15, NAT_1:13;
A20: [j,i] in Indices (Jordan_block (L,n)) by A1, A7, A16, ZFMISC_1:87;
(Col ((Jordan_block (L,n)),i)) . j = (Jordan_block (L,n)) * (j,i) by A3, A16, MATRIX_0:def 8
.= 0. K by A17, A19, A20, Def1 ;
hence (mlt ((Col ((Jordan_block (L,n)),i)),f)) . j = (0. K) * (f /. j) by A11, A16, A18, FVSUM_1:61
.= 0. K ;
:: thesis: verum

end;

hence (Col ((Jordan_block (L,n)),i)) "*" F = (mlt ((Col ((Jordan_block (L,n)),i)),f)) . i by A1, A11, MATRIX_3:12
.= ((Jordan_block (L,n)) * (i,i)) * (f /. i) by A1, A11, A13, FVSUM_1:61
.= L * (F /. i) by A14, Def1 ;
:: thesis: verum

end;

A21: i1 <> i ;
assume i <> 1 ; :: thesis: (Col ((Jordan_block (L,n)),i)) "*" F = (L * (F /. i)) + (F /. (i - 1))
then i1 + 1 > 0 + 1 by A2, XXREAL_0:1;
then i1 >= 1 by NAT_1:14;
then A22: i1 in Seg n by A6;
then A23: ( i1 + 1 = i & [i1,i] in Indices (Jordan_block (L,n)) ) by A1, A7, ZFMISC_1:87;

A24: now :: thesis: for j being Nat st j in Seg n & j <> i & j <> i1 holds
(mlt (Ci,f)) . j = 0. K

let j be Nat; :: thesis: ( j in Seg n & j <> i & j <> i1 implies (mlt (Ci,f)) . j = 0. K )
assume that
A25: j in Seg n and
A26: j <> i and
A27: j <> i1 ; :: thesis: (mlt (Ci,f)) . j = 0. K
( [j,i] in Indices (Jordan_block (L,n)) & j + 1 <> i ) by A1, A7, A25, A27, ZFMISC_1:87;
then A28: 0. K = (Jordan_block (L,n)) * (j,i) by A26, Def1
.= Ci . j by A3, A25, MATRIX_0:def 8 ;
f . j = f /. j by A9, A25, PARTFUN1:def 6;
hence (mlt (Ci,f)) . j = (0. K) * (f /. j) by A25, A28, FVSUM_1:61
.= 0. K ;
:: thesis: verum

end;

A29: f . i1 = f /. i1 by A9, A22, PARTFUN1:def 6;
A30: (Col ((Jordan_block (L,n)),i)) . i1 = (Jordan_block (L,n)) * (i1,i) by A3, A22, MATRIX_0:def 8;
(mlt (Ci,f)) /. i1 = (mlt (Ci,f)) . i1 by A11, A22, PARTFUN1:def 6
.= ((Jordan_block (L,n)) * (i1,i)) * (f /. i1) by A22, A30, A29, FVSUM_1:61
.= (1_ K) * (f /. i1) by A23, Def1
.= f /. i1 ;
hence (Col ((Jordan_block (L,n)),i)) "*" F = (L * (F /. i)) + (F /. (i - 1)) by A1, A11, A22, A21, A12, A24, MATRIX15:7; :: thesis: verum