let n be Nat; :: thesis: for M being Matrix of n, REAL holds Indices M = Indices |:M:|
let M be Matrix of n, REAL ; :: thesis: Indices M = Indices |:M:|
A1: ( len |:M:| = len M & width |:M:| = width M ) by Def7;
( Seg (len M) = dom M & Seg (len |:M:|) = dom |:M:| ) by FINSEQ_1:def 3;
hence Indices M = Indices |:M:| by A1; :: thesis: verum