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: Seg (len M) = dom M by FINSEQ_1:def 3;

( len |:M:| = len M & width |:M:| = width M ) by Def7;

hence Indices M = Indices |:M:| by A1, FINSEQ_1:def 3; :: thesis: verum

let M be Matrix of n,REAL; :: thesis: Indices M = Indices |:M:|

A1: Seg (len M) = dom M by FINSEQ_1:def 3;

( len |:M:| = len M & width |:M:| = width M ) by Def7;

hence Indices M = Indices |:M:| by A1, FINSEQ_1:def 3; :: thesis: verum