let n, m be Nat; 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 ; for M being Matrix of n,m,D holds M * (idseq n) = M
let M be Matrix of n,m,D; 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;
( [i,j] in Indices M implies M * (i,j) = (M * I) * (i,j) )
assume A3:
[i,j] in Indices M
;
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;
verum
end;
len (M * I) = len M
by Def4;
hence
M * (idseq n) = M
by A1, A2, MATRIX_0:21; verum