The following example deals with Legendre polynomials: from a differential equation and a mixed differential-difference equation that define them, elimination of yields a difference equation that vanishes on them.
Continuing this application, we derive a proof that Legendre polynomials satisfy
Indeed, it follows that the summand in the identity that we want to prove satisfies
in the new algebra . (Since the index of summation is , we consider polynomials in this variable to allow for its elimination.)
The previous equations are satisfied by the summand. Setting in them yields equations satisfied by the sum. A final Groebner basis calculation returns these equations:
Solving this simple system of PDEs yields the announced closed form.