for i, n being Nat st 1 <= i & i <= n holds
Sum (Base_FinSeq (n,i)) = 1