:: deftheorem defines -Matrices_over MATRIX_1:def 1 :
for K being non empty doubleLoopStr
for n being Nat holds n -Matrices_over K = n -tuples_on (n -tuples_on the carrier of K);