let n be Nat; :: thesis: for K being Field
for L being Element of K holds diagonal_of_Matrix (Jordan_block (L,n)) = n |-> L
let K be Field; :: thesis: for L being Element of K holds diagonal_of_Matrix (Jordan_block (L,n)) = n |-> L
let L be Element of K; :: thesis: diagonal_of_Matrix (Jordan_block (L,n)) = n |-> L
set B = Jordan_block (L,n);

A1: now :: thesis: for i being Nat st 1 <= i & i <= n holds
(diagonal_of_Matrix (Jordan_block (L,n))) . i = (n |-> L) . i

A2: [:(Seg n),(Seg n):] = Indices (Jordan_block (L,n)) by MATRIX_0:24;
let i be Nat; :: thesis: ( 1 <= i & i <= n implies (diagonal_of_Matrix (Jordan_block (L,n))) . i = (n |-> L) . i )
assume ( 1 <= i & i <= n ) ; :: thesis: (diagonal_of_Matrix (Jordan_block (L,n))) . i = (n |-> L) . i
then A3: i in Seg n ;
then A4: [i,i] in [:(Seg n),(Seg n):] by ZFMISC_1:87;
thus (diagonal_of_Matrix (Jordan_block (L,n))) . i = (Jordan_block (L,n)) * (i,i) by A3, MATRIX_3:def 10
.= L by A4, A2, Def1
.= (n |-> L) . i by A3, FINSEQ_2:57 ; :: thesis: verum

end;

( len (diagonal_of_Matrix (Jordan_block (L,n))) = n & len (n |-> L) = n ) by CARD_1:def 7, MATRIX_3:def 10;
hence diagonal_of_Matrix (Jordan_block (L,n)) = n |-> L by A1; :: thesis: verum