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