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)) ) )
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)) ) )
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;
A2: ( len (Jordan_block L,n) = n & dom (Jordan_block L,n) = Seg (len (Jordan_block L,n)) & Indices (Jordan_block L,n) = [:(Seg n),(Seg n):] ) by FINSEQ_1:def 3, MATRIX_1:25;
reconsider Ci = Col (Jordan_block L,n),i, f = F as Element of N -tuples_on the carrier of K by MATRIX_1:25;
A3: ( dom (mlt Ci,f) = Seg n & dom f = Seg n ) by FINSEQ_2:144;
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

assume A4: i = 1 ; :: thesis: (Col (Jordan_block L,n),i) "*" F = L * (F /. i)
A5: ( (Col (Jordan_block L,n),i) . i = (Jordan_block L,n) * i,i & [i,i] in Indices (Jordan_block L,n) & f . i = f /. i ) by A1, A2, A3, MATRIX_1:def 9, PARTFUN1:def 8, ZFMISC_1:106;

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 A6: ( j in Seg n & j <> i ) ; :: thesis: (mlt (Col (Jordan_block L,n),i),f) . j = 0. K
1 <= j by A6, FINSEQ_1:3;
then A7: i < j + 1 by A4, NAT_1:13;
A8: ( [j,i] in Indices (Jordan_block L,n) & f . j = f /. j ) by A1, A2, A3, A6, PARTFUN1:def 8, ZFMISC_1:106;
(Col (Jordan_block L,n),i) . j = (Jordan_block L,n) * j,i by A2, A6, MATRIX_1:def 9
.= 0. K by A7, A6, A8, Def1 ;
hence (mlt (Col (Jordan_block L,n),i),f) . j = (0. K) * (f /. j) by A3, A6, A8, 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, A3, MATRIX_3:14
.= ((Jordan_block L,n) * i,i) * (f /. i) by A1, A3, A5, FVSUM_1:74
.= L * (F /. i) by A5, Def1 ;
:: thesis: verum

end;

assume A9: i <> 1 ; :: thesis: (Col (Jordan_block L,n),i) "*" F = (L * (F /. i)) + (F /. (i - 1))
A10: ( n >= i & i >= 1 ) by A1, FINSEQ_1:3;
then reconsider i1 = i - 1 as Element of NAT by NAT_1:21;
i1 + 1 > 0 + 1 by A9, A10, XXREAL_0:1;
then ( i1 > 0 & i1 + 1 >= i1 ) by NAT_1:11;
then ( i1 >= 1 & n >= i1 ) by A10, NAT_1:14, XXREAL_0:2;
then A11: ( i1 in Seg n & i1 <> i ) ;
then A12: ( (Col (Jordan_block L,n),i) . i = (Jordan_block L,n) * i,i & (Col (Jordan_block L,n),i) . i1 = (Jordan_block L,n) * i1,i & i1 + 1 = i & [i,i] in Indices (Jordan_block L,n) & [i1,i] in Indices (Jordan_block L,n) & f . i = f /. i & f . i1 = f /. i1 ) by A1, A2, A3, MATRIX_1:def 9, PARTFUN1:def 8, ZFMISC_1:106;
A13: (mlt Ci,f) /. i = (mlt Ci,f) . i by A1, A3, PARTFUN1:def 8
.= ((Jordan_block L,n) * i,i) * (f /. i) by A1, A12, FVSUM_1:74
.= L * (f /. i) by A12, Def1 ;
A14: (mlt Ci,f) /. i1 = (mlt Ci,f) . i1 by A3, A11, PARTFUN1:def 8
.= ((Jordan_block L,n) * i1,i) * (f /. i1) by A11, A12, FVSUM_1:74
.= (1_ K) * (f /. i1) by A12, Def1
.= f /. i1 by VECTSP_1:def 13 ;

now

let j be Nat; :: thesis: ( j in Seg n & j <> i & j <> i1 implies (mlt Ci,f) . j = 0. K )
assume A15: ( j in Seg n & j <> i & j <> i1 ) ; :: thesis: (mlt Ci,f) . j = 0. K
A16: ( [j,i] in Indices (Jordan_block L,n) & f . j = f /. j & j + 1 <> i ) by A1, A2, A3, A15, PARTFUN1:def 8, ZFMISC_1:106;
then 0. K = (Jordan_block L,n) * j,i by A15, Def1
.= Ci . j by A2, A15, MATRIX_1:def 9 ;
hence (mlt Ci,f) . j = (0. K) * (f /. j) by A15, A16, FVSUM_1:74
.= 0. K by VECTSP_1:36 ;
:: thesis: verum

end;

hence (Col (Jordan_block L,n),i) "*" F = (L * (F /. i)) + (F /. (i - 1)) by A1, A3, A11, A13, A14, MATRIX15:7; :: thesis: verum