let n, i 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 13;
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:3;
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_1:25;
then A4: (Col (Jordan_block L,n),i) . i = (Jordan_block L,n) * i,i by A1, MATRIX_1:def 9;
A5: i1 + 1 >= i1 by NAT_1:11;
n >= i by A1, FINSEQ_1:3;
then A6: n >= i1 by A5, XXREAL_0:2;
A7: Indices (Jordan_block L,n) = [:(Seg n),(Seg n):] by MATRIX_1:25;
then A8: [i,i] in Indices (Jordan_block L,n) by A1, ZFMISC_1:106;
reconsider Ci = Col (Jordan_block L,n),i, f = F as Element of N -tuples_on the carrier of K by MATRIX_1:25;
A9: dom f = Seg n by FINSEQ_2:144;
then A10: f . i = f /. i by A1, PARTFUN1:def 8;
A11: dom (mlt Ci,f) = Seg n by FINSEQ_2:144;
then A12: (mlt Ci,f) /. i = (mlt Ci,f) . i by A1, PARTFUN1:def 8
.= ((Jordan_block L,n) * i,i) * (f /. i) by A1, A4, A10, FVSUM_1:74
.= 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_1:def 9, PARTFUN1:def 8;
A14: [i,i] in Indices (Jordan_block L,n) by A1, A7, ZFMISC_1:106;
assume A15: i = 1 ; :: thesis: (Col (Jordan_block L,n),i) "*" F = L * (F /. i)

now

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 8;
1 <= j by A16, FINSEQ_1:3;
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:106;
(Col (Jordan_block L,n),i) . j = (Jordan_block L,n) * j,i by A3, A16, MATRIX_1:def 9
.= 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:74
.= 0. K by VECTSP_1:36 ;
:: 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:14
.= ((Jordan_block L,n) * i,i) * (f /. i) by A1, A11, A13, FVSUM_1:74
.= 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:106;

A24: now

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:106;
then A28: 0. K = (Jordan_block L,n) * j,i by A26, Def1
.= Ci . j by A3, A25, MATRIX_1:def 9 ;
f . j = f /. j by A9, A25, PARTFUN1:def 8;
hence (mlt Ci,f) . j = (0. K) * (f /. j) by A25, A28, FVSUM_1:74
.= 0. K by VECTSP_1:36 ;
:: thesis: verum

end;

A29: f . i1 = f /. i1 by A9, A22, PARTFUN1:def 8;
A30: (Col (Jordan_block L,n),i) . i1 = (Jordan_block L,n) * i1,i by A3, A22, MATRIX_1:def 9;
(mlt Ci,f) /. i1 = (mlt Ci,f) . i1 by A11, A22, PARTFUN1:def 8
.= ((Jordan_block L,n) * i1,i) * (f /. i1) by A22, A30, A29, FVSUM_1:74
.= (1_ K) * (f /. i1) by A23, Def1
.= f /. i1 by VECTSP_1:def 13 ;
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