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 that
A1: i in Seg n and
A2: i <> n ; :: thesis: Line (Jordan_block L,n),i = (L * (Line (1. K,n),i)) + (Line (1. K,n),(i + 1))
reconsider N = n as Element of NAT by ORDINAL1:def 13;
set J = Jordan_block L,n;
set i1 = i + 1;
set ONE = 1. K,n;
set Li = Line (1. K,n),i;
set Li1 = Line (1. K,n),(i + 1);
set LJ = Line (Jordan_block L,n),i;
A3: width (1. K,n) = n by MATRIX_1:25;
A4: Indices (1. K,n) = Indices (Jordan_block L,n) by 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;
A5: Indices (1. K,n) = [:(Seg n),(Seg n):] by MATRIX_1:25;
A6: width (Jordan_block L,n) = n by MATRIX_1:25;

now

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

now

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

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

then A14: i + 1 > j by NAT_1:13;
thus LJ . j = L by A5, A4, A9, A12, A13, 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 A5, A9, A13, MATRIX_1:def 12
.= ((L * Li) + Li1) . j by A5, A10, A11, A14, MATRIX_1:def 12 ; :: thesis: verum

end;

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

then A16: i < j by NAT_1:13;
thus LJ . j = 1_ K by A5, A4, A9, A12, A15, 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 A5, A9, A16, MATRIX_1:def 12
.= ((L * Li) + Li1) . j by A5, A10, A11, A15, MATRIX_1:def 12 ; :: thesis: verum

end;

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

hence LJ . j = 0. K by A5, A4, A9, A12, 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 A5, A9, A17, MATRIX_1:def 12
.= ((L * Li) + Li1) . j by A5, A10, A11, A17, 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