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

A2: [:(Seg n),(Seg n):] = Indices (Jordan_block L,n) by MATRIX_1:25;
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 by FINSEQ_1:3;
then A4: [i,i] in [:(Seg n),(Seg n):] by ZFMISC_1:106;
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:71 ; :: thesis: verum

end;

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