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