let i, n be Nat; :: thesis: for K being Field
for L being Element of K st i in Seg n & i <> n holds
Line (Jordan_block L,n),i = (L * (Line (1. K,n),i)) + (Line (1. K,n),(i + 1))
let K be Field; :: thesis: for L being Element of K st i in Seg n & i <> n holds
Line (Jordan_block L,n),i = (L * (Line (1. K,n),i)) + (Line (1. K,n),(i + 1))
let L be Element of K; :: thesis: ( i in Seg n & i <> n implies Line (Jordan_block L,n),i = (L * (Line (1. K,n),i)) + (Line (1. K,n),(i + 1)) )
assume A1: ( i in Seg n & i <> n ) ; :: thesis: Line (Jordan_block L,n),i = (L * (Line (1. K,n),i)) + (Line (1. K,n),(i + 1))
set ONE = 1. K,n;
set i1 = i + 1;
set Li = Line (1. K,n),i;
set Li1 = Line (1. K,n),(i + 1);
set J = Jordan_block L,n;
set LJ = Line (Jordan_block L,n),i;
reconsider N = n as Element of NAT by ORDINAL1:def 13;
A2: ( width (1. K,n) = n & width (Jordan_block L,n) = n & Indices (1. K,n) = [:(Seg n),(Seg n):] & Indices (1. K,n) = Indices (Jordan_block L,n) ) by MATRIX_1:25, MATRIX_1:27;
reconsider Li = Line (1. K,n),i, Li1 = Line (1. K,n),(i + 1), LJ = Line (Jordan_block L,n),i as Element of N -tuples_on the carrier of K by MATRIX_1:25;

now

let j be Nat; :: thesis: ( j in Seg n implies ((L * Li) + Li1) . j = LJ . j )
assume A3: j in Seg n ; :: thesis: ((L * Li) + Li1) . j = LJ . j
i <= n by A1, FINSEQ_1:3;
then i < n by A1, XXREAL_0:1;
then ( 1 <= i + 1 & i + 1 <= n ) by NAT_1:11, NAT_1:13;
then i + 1 in Seg n ;
then A4: ( [i,j] in [:(Seg n),(Seg n):] & [(i + 1),j] in [:(Seg n),(Seg n):] ) by A1, A3, ZFMISC_1:106;
A5: ( Li . j = (1. K,n) * i,j & Li1 . j = (1. K,n) * (i + 1),j & LJ . j = (Jordan_block L,n) * i,j ) by A2, A3, MATRIX_1:def 8;
then (L * Li) . j = L * ((1. K,n) * i,j) by A3, FVSUM_1:63;
then A6: ((L * Li) + Li1) . j = (L * ((1. K,n) * i,j)) + ((1. K,n) * (i + 1),j) by A3, A5, FVSUM_1:22;

now

per cases ( i = j or i + 1 = j or ( i <> j & i + 1 <> j ) ) ;

suppose A7: i = j ; :: thesis: LJ . j = ((L * Li) + Li1) . j

then A8: i + 1 > j by NAT_1:13;
thus LJ . j = L by A2, A4, A5, A7, Def1
.= L + (0. K) by RLVECT_1:def 7
.= (L * (1_ K)) + (0. K) by VECTSP_1:def 19
.= (L * ((1. K,n) * i,j)) + (0. K) by A2, A4, A7, MATRIX_1:def 12
.= ((L * Li) + Li1) . j by A2, A4, A6, A8, MATRIX_1:def 12 ; :: thesis: verum

end;

suppose A9: i + 1 = j ; :: thesis: LJ . j = ((L * Li) + Li1) . j

then A10: i < j by NAT_1:13;
thus LJ . j = 1_ K by A2, A4, A5, A9, Def1
.= (0. K) + (1_ K) by RLVECT_1:def 7
.= (L * (0. K)) + (1_ K) by VECTSP_1:39
.= (L * ((1. K,n) * i,j)) + (1_ K) by A2, A4, A10, MATRIX_1:def 12
.= ((L * Li) + Li1) . j by A2, A4, A6, A9, MATRIX_1:def 12 ; :: thesis: verum

end;

suppose A11: ( i <> j & i + 1 <> j ) ; :: thesis: LJ . j = ((L * Li) + Li1) . j

hence LJ . j = 0. K by A2, A4, A5, Def1
.= (0. K) + (0. K) by RLVECT_1:def 7
.= (L * (0. K)) + (0. K) by VECTSP_1:39
.= (L * ((1. K,n) * i,j)) + (0. K) by A2, A4, A11, MATRIX_1:def 12
.= ((L * Li) + Li1) . j by A2, A4, A6, A11, MATRIX_1:def 12 ;
:: thesis: verum

end;

end;

end;

hence ((L * Li) + Li1) . j = LJ . j ; :: thesis: verum

end;

hence Line (Jordan_block L,n),i = (L * (Line (1. K,n),i)) + (Line (1. K,n),(i + 1)) by FINSEQ_2:139; :: thesis: verum