A proof by induction of Jim's identity is probably what you want. Multiply by both sides by {((a - k), (b - (n - k)))} and use the fact that

FactorialPower[a, k + 1] == (a - k) FactorialPower[a, k]

etc. to get terms like

Binomial[n, k] FactorialPower[a, k + 1] FactorialPower[b, -k + n] 
Binomial[n, k] FactorialPower[a, k] FactorialPower[b, -k + n + 1]

Shift the index of the first type to get terms like

Binomial[n, k - 1] FactorialPower[a, k] FactorialPower[b, -k + n + 1]

Then use the binomial identity for Binomial[n, k - 1] Binomial[n, k] to write the LHS as a sum up to n + 1.

Because your example was a special case of the more general expansion, it wasn't clear that you were aware of that identity. In the link I used the "Sheffer Sequence" is referenced and a search on that term might find some established proofs. Wolfram MathWorld gives a blurb on the Sheffer Sequence.

I'm not sure what you would expect from Mathematica. If FullSimplify ended up with FactorialPower[1, n], how would the "black box" function FullSimplify be considered a proof?

P.S. To clarify why I'm not satisfied with Rudin's proof (though I accept its validity):

The problem I've stated at the top entails only a finite sum of rational numbers. No infinite sums. No irrational numbers. No need to define the real numbers in order to state the problem. Yet Rudin's proof depends on the theory of real numbers. I'm hoping to find a way to a proof that doesn't depend on the theory of real numbers.

Thank you. I recognize the relation of my problem to the Binomial Expansion:

In[18]:= FullSimplify[
 Binomial[n, k] FactorialPower[1/2, k] FactorialPower[1/2, n - k] == 
  n!*Binomial[1/2, k]*Binomial[1/2, n - k]]

Out[18]= True

and that equation I can prove easily.

Curiously---but not essentially to my line of inquiry---Mathematica doesn't solve the sum when I express it more like the Binomial Expansion:

In[13]:= FullSimplify[n!*Binomial[1/2, k]*Binomial[1/2, n - k]]

Out[13]= Binomial[1/2, k] Binomial[1/2, -k + n] n!

or more simply:

In[13]:= FullSimplify[Binomial[1/2, k]*Binomial[1/2, n - k]]

Out[13]= Binomial[1/2, k] Binomial[1/2, -k + n] n!

I could solve my problem (finding a proof as described in my initial post) by working through an analysis textbook; but what I'm really after is a proof that doesn't rely on derivatives. A proof modeled after (e.g.) Rudin would make heavy use of derivatives and Taylor's Theorem, which I'm trying to avoid.

I was hoping Mathematica could help me find such a proof, but my hope is a long shot, as Mathematica seems to excel at calculating true answers, but less so at providing proofs.