let n be Nat; :: thesis: for K being Field
for M1 being Matrix of n,K holds Trace M1 = Trace (M1 @)
let K be Field; :: thesis: for M1 being Matrix of n,K holds Trace M1 = Trace (M1 @)
let M1 be Matrix of n,K; :: thesis: Trace M1 = Trace (M1 @)
A1: for i being Nat st i in Seg n holds
(diagonal_of_Matrix M1) . i = (diagonal_of_Matrix (M1 @)) . i

proof

let i be Nat; :: thesis: ( i in Seg n implies (diagonal_of_Matrix M1) . i = (diagonal_of_Matrix (M1 @)) . i )
assume A2: i in Seg n ; :: thesis: (diagonal_of_Matrix M1) . i = (diagonal_of_Matrix (M1 @)) . i
then A3: ( (diagonal_of_Matrix M1) . i = M1 * (i,i) & (diagonal_of_Matrix (M1 @)) . i = (M1 @) * (i,i) ) by MATRIX_3:def 10;
Indices M1 = [:(Seg n),(Seg n):] by MATRIX_0:24;
then [i,i] in Indices M1 by A2, ZFMISC_1:87;
hence (diagonal_of_Matrix M1) . i = (diagonal_of_Matrix (M1 @)) . i by A3, MATRIX_0:def 6; :: thesis: verum

end;

len (diagonal_of_Matrix (M1 @)) = n by MATRIX_3:def 10;
then A4: dom (diagonal_of_Matrix (M1 @)) = Seg n by FINSEQ_1:def 3;
len (diagonal_of_Matrix M1) = n by MATRIX_3:def 10;
then dom (diagonal_of_Matrix M1) = Seg n by FINSEQ_1:def 3;
hence Trace M1 = Trace (M1 @) by A1, A4, FINSEQ_1:13; :: thesis: verum