let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K holds diagonal_of_Matrix M = diagonal_of_Matrix (M @ )
let K be Field; :: thesis: for M being Matrix of n,K holds diagonal_of_Matrix M = diagonal_of_Matrix (M @ )
let M be Matrix of n,K; :: thesis: diagonal_of_Matrix M = diagonal_of_Matrix (M @ )
set DM = diagonal_of_Matrix M;
set DM9 = diagonal_of_Matrix (M @ );
A1: len (diagonal_of_Matrix M) = n by MATRIX_3:def 10;

A2: now

let i be Nat; :: thesis: ( 1 <= i & i <= len (diagonal_of_Matrix M) implies (diagonal_of_Matrix M) . i = (diagonal_of_Matrix (M @ )) . i )
assume that
A3: 1 <= i and
A4: i <= len (diagonal_of_Matrix M) ; :: thesis: (diagonal_of_Matrix M) . i = (diagonal_of_Matrix (M @ )) . i
i in NAT by ORDINAL1:def 13;
then A5: i in Seg n by A1, A3, A4;
then A6: (diagonal_of_Matrix (M @ )) . i = (M @ ) * i,i by MATRIX_3:def 10;
Indices M = [:(Seg n),(Seg n):] by MATRIX_1:25;
then A7: [i,i] in Indices M by A5, ZFMISC_1:106;
(diagonal_of_Matrix M) . i = M * i,i by A5, MATRIX_3:def 10;
hence (diagonal_of_Matrix M) . i = (diagonal_of_Matrix (M @ )) . i by A7, A6, MATRIX_1:def 7; :: thesis: verum

end;

len (diagonal_of_Matrix (M @ )) = n by MATRIX_3:def 10;
hence diagonal_of_Matrix M = diagonal_of_Matrix (M @ ) by A1, A2, FINSEQ_1:18; :: thesis: verum