Only the recursions are given for each step, since the certificates are extremely long.

>	f := (n, r, s) ->(-1)^(n+r+s)*binomial(n,r)*binomial(n,s)*binomial(n+r,r)*binomial(n+s,s)*binomial(2*n-r-s,n);

>	Rec1 := iSum(2, f(n,r,s), [N,R,S], [n,r,s]);

>	g := (n,k) -> binomial(n,k)^4;

>	Rec2 := iSum(2, g(n,k), [N,K], [n,k]);

>

Since the recursions in Rec1 and Rec2 are the same, and both $\sum_{r,s}f(n,r,s)$ and $\sum_{k} g(n,k) $ satisfy the same intial condition, we have proved
$\sum_{r,s}f(n,r,s) = \sum_{k} g(n,k)$

(A=B, page 33)