theorem Th19: :: MATRTOP1:19

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