for n being Nat
for K being Field holds len (MX2FinS (1. (K,n))) = n