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 <> n implies (Line (Jordan_block L,n),i) "*" F = (L * (F /. i)) + (F /. (i + 1)) ) & ( i = n implies (Line (Jordan_block L,n),i) "*" F = L * (F /. i) ) )
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 <> n implies (Line (Jordan_block L,n),i) "*" F = (L * (F /. i)) + (F /. (i + 1)) ) & ( i = n implies (Line (Jordan_block L,n),i) "*" F = L * (F /. i) ) )
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 <> n implies (Line (Jordan_block L,n),i) "*" F = (L * (F /. i)) + (F /. (i + 1)) ) & ( i = n implies (Line (Jordan_block L,n),i) "*" F = L * (F /. i) ) )
let F be Element of n -tuples_on the carrier of K; :: thesis: ( i in Seg n implies ( ( i <> n implies (Line (Jordan_block L,n),i) "*" F = (L * (F /. i)) + (F /. (i + 1)) ) & ( i = n implies (Line (Jordan_block L,n),i) "*" F = L * (F /. i) ) ) )
assume A1: i in Seg n ; :: thesis: ( ( i <> n implies (Line (Jordan_block L,n),i) "*" F = (L * (F /. i)) + (F /. (i + 1)) ) & ( i = n implies (Line (Jordan_block L,n),i) "*" F = L * (F /. i) ) )
set J = Jordan_block L,n;
set Li = Line (Jordan_block L,n),i;
reconsider N = n as Element of NAT by ORDINAL1:def 13;
A2: ( width (Jordan_block L,n) = n & Indices (Jordan_block L,n) = [:(Seg n),(Seg n):] ) by MATRIX_1:25;
reconsider Li = Line (Jordan_block L,n),i, f = F as Element of N -tuples_on the carrier of K by MATRIX_1:25;
A3: ( dom (mlt Li,f) = Seg n & dom f = Seg n ) by FINSEQ_2:144;
thus ( i <> n implies (Line (Jordan_block L,n),i) "*" F = (L * (F /. i)) + (F /. (i + 1)) ) :: thesis: ( i = n implies (Line (Jordan_block L,n),i) "*" F = L * (F /. i) )

proof

assume A4: i <> n ; :: thesis: (Line (Jordan_block L,n),i) "*" F = (L * (F /. i)) + (F /. (i + 1))
i <= n by A1, FINSEQ_1:3;
then i < n by A4, XXREAL_0:1;
then ( 1 <= i + 1 & i + 1 <= n ) by NAT_1:11, NAT_1:13;
then A5: ( i + 1 in Seg n & i + 1 > i ) by NAT_1:13;
then A6: ( [i,i] in Indices (Jordan_block L,n) & [i,(i + 1)] in Indices (Jordan_block L,n) & f . i = f /. i & f . (i + 1) = f /. (i + 1) & (Jordan_block L,n) * i,i = Li . i & (Jordan_block L,n) * i,(i + 1) = Li . (i + 1) ) by A1, A2, A3, MATRIX_1:def 8, PARTFUN1:def 8, ZFMISC_1:106;
A7: (mlt Li,f) /. i = (mlt Li,f) . i by A1, A3, PARTFUN1:def 8
.= ((Jordan_block L,n) * i,i) * (f /. i) by A1, A6, FVSUM_1:74
.= L * (f /. i) by A6, Def1 ;
A8: (mlt Li,f) /. (i + 1) = (mlt Li,f) . (i + 1) by A3, A5, PARTFUN1:def 8
.= ((Jordan_block L,n) * i,(i + 1)) * (f /. (i + 1)) by A5, A6, FVSUM_1:74
.= (1_ K) * (f /. (i + 1)) by A6, Def1
.= f /. (i + 1) by VECTSP_1:def 13 ;

now

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

end;

hence (Line (Jordan_block L,n),i) "*" F = (L * (F /. i)) + (F /. (i + 1)) by A1, A5, A7, A8, A3, MATRIX15:7; :: thesis: verum

end;

assume A11: i = n ; :: thesis: (Line (Jordan_block L,n),i) "*" F = L * (F /. i)
A12: ( (Line (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 8, PARTFUN1:def 8, ZFMISC_1:106;

now

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

end;

hence (Line (Jordan_block L,n),i) "*" F = (mlt (Line (Jordan_block L,n),i),f) . i by A1, A3, MATRIX_3:14
.= ((Jordan_block L,n) * i,i) * (f /. i) by A12, A1, A3, FVSUM_1:74
.= L * (F /. i) by A12, Def1 ;
:: thesis: verum