let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K
for I being Element of Permutations n st I = idseq n holds
diagonal_of_Matrix M = Path_matrix (I,M)
let K be Field; :: thesis: for M being Matrix of n,K
for I being Element of Permutations n st I = idseq n holds
diagonal_of_Matrix M = Path_matrix (I,M)
let M be Matrix of n,K; :: thesis: for I being Element of Permutations n st I = idseq n holds
diagonal_of_Matrix M = Path_matrix (I,M)
let I be Element of Permutations n; :: thesis: ( I = idseq n implies diagonal_of_Matrix M = Path_matrix (I,M) )
assume A1: I = idseq n ; :: thesis: diagonal_of_Matrix M = Path_matrix (I,M)
set P = Path_matrix (I,M);
set D = diagonal_of_Matrix M;
A2: len (Path_matrix (I,M)) = n by MATRIX_3:def 7;

A3: now :: thesis: for i being Nat st 1 <= i & i <= n holds
(Path_matrix (I,M)) . i = (diagonal_of_Matrix M) . i

let i be Nat; :: thesis: ( 1 <= i & i <= n implies (Path_matrix (I,M)) . i = (diagonal_of_Matrix M) . i )
assume that
A4: 1 <= i and
A5: i <= n ; :: thesis: (Path_matrix (I,M)) . i = (diagonal_of_Matrix M) . i
A6: i in Seg n by A4, A5;
then A7: I . i = i by A1, FINSEQ_2:49;
i in dom (Path_matrix (I,M)) by A2, A6, FINSEQ_1:def 3;
then (Path_matrix (I,M)) . i = M * (i,i) by A7, MATRIX_3:def 7;
hence (Path_matrix (I,M)) . i = (diagonal_of_Matrix M) . i by A6, MATRIX_3:def 10; :: thesis: verum

end;

len (diagonal_of_Matrix M) = n by MATRIX_3:def 10;
hence diagonal_of_Matrix M = Path_matrix (I,M) by A2, A3; :: thesis: verum