:: deftheorem defines MX2FinS MATRIX13:def 6 :
for K being Field
for m, n being Nat
for M being Matrix of m,n,K holds MX2FinS M = M;