for n being Nat
for M being Matrix of n,REAL holds Indices M = Indices |:M:|