:: deftheorem defines Indices MATRIX_0:def 4 :
for M being tabular FinSequence holds Indices M = [:(dom M),(Seg (width M)):];