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 :: thesis: for i being Nat st 1 <= i & i <= len (diagonal_of_Matrix M) holds
(diagonal_of_Matrix M) . i = (diagonal_of_Matrix (M @)) . i

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
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_0:24;
then A7: [i,i] in Indices M by A5, ZFMISC_1:87;
(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_0:def 6; :: 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; :: thesis: verum