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