let n be Nat; :: thesis: for K being Field
for L being Element of K holds Line ((Jordan_block (L,n)),n) = L * (Line ((1. (K,n)),n))
let K be Field; :: thesis: for L being Element of K holds Line ((Jordan_block (L,n)),n) = L * (Line ((1. (K,n)),n))
let L be Element of K; :: thesis: Line ((Jordan_block (L,n)),n) = L * (Line ((1. (K,n)),n))
set ONE = 1. (K,n);
set Ln = Line ((1. (K,n)),n);
set J = Jordan_block (L,n);
set LJ = Line ((Jordan_block (L,n)),n);
reconsider N = n as Element of NAT by ORDINAL1:def 12;
A1: width (Jordan_block (L,n)) = n by MATRIX_0:24;
A2: Indices (1. (K,n)) = Indices (Jordan_block (L,n)) by MATRIX_0:26;
reconsider Ln = Line ((1. (K,n)),n), LJ = Line ((Jordan_block (L,n)),n) as Element of N -tuples_on the carrier of K by MATRIX_0:24;
A3: Indices (1. (K,n)) = [:(Seg n),(Seg n):] by MATRIX_0:24;
A4: width (1. (K,n)) = n by MATRIX_0:24;

now :: thesis: for j being Nat st j in Seg n holds
(L * Ln) . j = LJ . j

let j be Nat; :: thesis: ( j in Seg n implies (L * Ln) . j = LJ . j )
assume A5: j in Seg n ; :: thesis: (L * Ln) . j = LJ . j
n <> 0 by A5;
then n in Seg n by FINSEQ_1:3;
then A6: [n,j] in [:(Seg n),(Seg n):] by A5, ZFMISC_1:87;
Ln . j = (1. (K,n)) * (n,j) by A4, A5, MATRIX_0:def 7;
then A7: (L * Ln) . j = L * ((1. (K,n)) * (n,j)) by A5, FVSUM_1:51;
A8: LJ . j = (Jordan_block (L,n)) * (n,j) by A1, A5, MATRIX_0:def 7;

now :: thesis: LJ . j = (L * Ln) . j

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

suppose A9: n = j ; :: thesis: LJ . j = (L * Ln) . j

hence LJ . j = L by A3, A2, A6, A8, Def1
.= L * (1_ K)
.= (L * Ln) . j by A3, A6, A7, A9, MATRIX_1:def 3 ;
:: thesis: verum

end;

suppose n + 1 = j ; :: thesis: (L * Ln) . j = LJ . j

then j > n by NAT_1:13;
hence (L * Ln) . j = LJ . j by A5, FINSEQ_1:1; :: thesis: verum

end;

suppose A10: ( n <> j & n + 1 <> j ) ; :: thesis: LJ . j = (L * Ln) . j

hence LJ . j = 0. K by A3, A2, A6, A8, Def1
.= L * (0. K)
.= (L * Ln) . j by A3, A6, A7, A10, MATRIX_1:def 3 ;
:: thesis: verum

end;

end;

end;

hence (L * Ln) . j = LJ . j ; :: thesis: verum

end;

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