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

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
i in NAT by ORDINAL1:def 13;
then A6: i in Seg n by A4, A5;
then A7: I . i = i by A1, FINSEQ_2:57;
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, FINSEQ_1:18; :: thesis: verum