let m, n be Nat; :: thesis: for D being non empty set
for M being Matrix of n,m,D holds M * (idseq n) = M
let D be non empty set ; :: thesis: for M being Matrix of n,m,D holds M * (idseq n) = M
let M be Matrix of n,m,D; :: thesis: M * (idseq n) = M
reconsider I = idseq n as Permutation of (Seg n) ;
A1: ( len (M * I) = len M & width (M * I) = width M ) by Def4;
for i, j being Nat st [i,j] in Indices M holds
M * i,j = (M * I) * i,j

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices M implies M * i,j = (M * I) * i,j )
assume A2: [i,j] in Indices M ; :: thesis: M * i,j = (M * I) * i,j
consider k being Nat such that
A3: ( I . i = k & [k,j] in Indices M & (M * I) * i,j = M * k,j ) by A2, Th37;
[i,j] in [:(Seg n),(Seg (width M)):] by A2, MATRIX_1:26;
then i in Seg n by ZFMISC_1:106;
hence M * i,j = (M * I) * i,j by A3, FUNCT_1:34; :: thesis: verum

end;

hence M * (idseq n) = M by A1, MATRIX_1:21; :: thesis: verum