theorem Th23: :: MATRIX14:23

for K being Field
for n, i being Nat holds len (Base_FinSeq (K,n,i)) = n