theorem :: NEWTON07:81

for n being non zero Nat holds Sum (RHartr n) = n * (2 |^ (n - 1))