theorem Th74: :: MATRIXR2:74

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