let n, m 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_0:25;
then A4: i in Seg n by ZFMISC_1:87;
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:17; :: thesis: verum

end;

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