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 <> 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);
A2: width (Jordan_block (L,n)) = n by MATRIX_0:24;
then A3: (Line ((Jordan_block (L,n)),i)) . i = (Jordan_block (L,n)) * (i,i) by A1, MATRIX_0:def 7;
A4: Indices (Jordan_block (L,n)) = [:(Seg n),(Seg n):] by MATRIX_0:24;
then A5: [i,i] in Indices (Jordan_block (L,n)) by A1, ZFMISC_1:87;
reconsider N = n as Element of NAT by ORDINAL1:def 12;
set Li = Line ((Jordan_block (L,n)),i);
reconsider Li = Line ((Jordan_block (L,n)),i), f = F as Element of N -tuples_on the carrier of K by MATRIX_0:24;
A6: dom f = Seg n by FINSEQ_2:124;
then A7: f . i = f /. i by A1, PARTFUN1:def 6;
A8: dom (mlt (Li,f)) = Seg n by FINSEQ_2:124;
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

A9: now :: thesis: for j being Nat st j in Seg n & j <> i & j <> i + 1 holds
(mlt (Li,f)) . j = 0. K

let j be Nat; :: thesis: ( j in Seg n & j <> i & j <> i + 1 implies (mlt (Li,f)) . j = 0. K )
assume that
A10: j in Seg n and
A11: ( j <> i & j <> i + 1 ) ; :: thesis: (mlt (Li,f)) . j = 0. K
[i,j] in Indices (Jordan_block (L,n)) by A1, A4, A10, ZFMISC_1:87;
then A12: 0. K = (Jordan_block (L,n)) * (i,j) by A11, Def1
.= Li . j by A2, A10, MATRIX_0:def 7 ;
f . j = f /. j by A6, A10, PARTFUN1:def 6;
hence (mlt (Li,f)) . j = (0. K) * (f /. j) by A10, A12, FVSUM_1:61
.= 0. K ;
:: thesis: verum

end;

A13: [i,i] in Indices (Jordan_block (L,n)) by A1, A4, ZFMISC_1:87;
assume A14: i <> n ; :: thesis: (Line ((Jordan_block (L,n)),i)) "*" F = (L * (F /. i)) + (F /. (i + 1))
i <= n by A1, FINSEQ_1:1;
then i < n by A14, XXREAL_0:1;
then ( 1 <= i + 1 & i + 1 <= n ) by NAT_1:11, NAT_1:13;
then A15: i + 1 in Seg n ;
then A16: [i,(i + 1)] in Indices (Jordan_block (L,n)) by A1, A4, ZFMISC_1:87;
A17: ( f . i = f /. i & (Jordan_block (L,n)) * (i,i) = Li . i ) by A1, A2, A6, MATRIX_0:def 7, PARTFUN1:def 6;
A18: (mlt (Li,f)) /. i = (mlt (Li,f)) . i by A1, A8, PARTFUN1:def 6
.= ((Jordan_block (L,n)) * (i,i)) * (f /. i) by A1, A17, FVSUM_1:61
.= L * (f /. i) by A13, Def1 ;
A19: i + 1 > i by NAT_1:13;
A20: ( f . (i + 1) = f /. (i + 1) & (Jordan_block (L,n)) * (i,(i + 1)) = Li . (i + 1) ) by A2, A6, A15, MATRIX_0:def 7, PARTFUN1:def 6;
(mlt (Li,f)) /. (i + 1) = (mlt (Li,f)) . (i + 1) by A8, A15, PARTFUN1:def 6
.= ((Jordan_block (L,n)) * (i,(i + 1))) * (f /. (i + 1)) by A15, A20, FVSUM_1:61
.= (1_ K) * (f /. (i + 1)) by A16, Def1
.= f /. (i + 1) ;
hence (Line ((Jordan_block (L,n)),i)) "*" F = (L * (F /. i)) + (F /. (i + 1)) by A1, A8, A15, A19, A18, A9, MATRIX15:7; :: thesis: verum

end;

assume A21: i = n ; :: thesis: (Line ((Jordan_block (L,n)),i)) "*" F = L * (F /. i)

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

let j be Nat; :: thesis: ( j in Seg n & j <> i implies (mlt ((Line ((Jordan_block (L,n)),i)),f)) . j = 0. K )
assume that
A22: j in Seg n and
A23: j <> i ; :: thesis: (mlt ((Line ((Jordan_block (L,n)),i)),f)) . j = 0. K
A24: f . j = f /. j by A6, A22, PARTFUN1:def 6;
j <= n by A22, FINSEQ_1:1;
then A25: j < i + 1 by A21, NAT_1:13;
A26: [i,j] in Indices (Jordan_block (L,n)) by A1, A4, A22, ZFMISC_1:87;
(Line ((Jordan_block (L,n)),i)) . j = (Jordan_block (L,n)) * (i,j) by A2, A22, MATRIX_0:def 7
.= 0. K by A23, A25, A26, Def1 ;
hence (mlt ((Line ((Jordan_block (L,n)),i)),f)) . j = (0. K) * (f /. j) by A8, A22, A24, FVSUM_1:61
.= 0. K ;
:: thesis: verum

end;

hence (Line ((Jordan_block (L,n)),i)) "*" F = (mlt ((Line ((Jordan_block (L,n)),i)),f)) . i by A1, A8, MATRIX_3:12
.= ((Jordan_block (L,n)) * (i,i)) * (f /. i) by A1, A8, A3, A7, FVSUM_1:61
.= L * (F /. i) by A5, Def1 ;
:: thesis: verum