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: width (M * I) = width M by Def4;
A2: 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 A3: [i,j] in Indices M ; :: thesis: M * i,j = (M * I) * i,j
[i,j] in [:(Seg n),(Seg (width M)):] by A3, MATRIX_1:26;
then A4: i in Seg n by ZFMISC_1:106;
ex k being Nat st
( I . i = k & [k,j] in Indices M & (M * I) * i,j = M * k,j ) by A3, Th37;
hence M * i,j = (M * I) * i,j by A4, FUNCT_1:34; :: thesis: verum

end;

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