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