let n be non zero Nat; :: thesis: Sum (RHartr n) = n * (2 |^ (n - 1))
Sum (RHartr n) = n * (Sum (Newton_Coeff (n - 1))) by RVSUM_1:87;
hence Sum (RHartr n) = n * (2 |^ (n - 1)) by NEWTON:32; :: thesis: verum