The source for this problem is Donald Knuth, The Art of
Computer Programming, Volume 1 Fundamental Algorithms, Third
Edition. His Example 2., page 30 begins with a proof that

n å
i = 0


i å
j = 0

a_{i}a_{j} = 
n å
i = 0


n å
j = i

a_{i}a_{j} . 

Its proof is in the vein of the fourth problem
on the fourth assignment.
It is formulated in the notation of the text as
(+i  0 £ i £ n:(+j  0 £ j £ i : a[i]a[j])) = (+i  0 £ i £ n:(+j  i £ j £ n : a[i]a[j])) . 



(+i  0 £ i £ n:(+j  0 £ j £ i : a[i]a[j])) 
 



(8.20), j d.n.o.f. in 0 £ i £ n. 




 

(+i,j  (0 £ i £ n) Ù(0 £ j £ i) : a[i]a[j]) 
 



Axiom, (*x,y  P:Q ) = (*y,x  P:Q ) 




 

(+j,i  (0 £ i £ n) Ù(0 £ j £ i) : a[i]a[j]) 
 


á

Lemma: (0 £ i £ n) Ù(0 £ j £ i) º (0 £ j £ n) Ù(j £ i £ n), 

Leibniz 8.12. Proof of Lemma appears below. 


ñ


 

(+j,i  (0 £ j £ n) Ù(j £ i £ n) : a[i]a[j]) 
 



(8.20), i d.n.o.f. in 0 £ j £ n. 




 

(+j  0 £ j £ n:( +i  j £ i £ n : a[i]a[j])) 
 



(8.21) applied four times (see below) 




 

(+i  0 £ i £ n:( +j  i £ j £ n : a[j]a[i])) 
 



Arithmetic, a[j]a[i] = a[i]a[j] 




 

(+i  0 £ i £ n:( +j  i £ j £ n : a[i]a[j])) 
 

Now for the proof of the Lemma:


 

 

(0 £ i) Ù(i £ n) Ù(0 £ j) Ù(j £ i) 
 


á

 (j £ i)Ù(i £ n) Þ (j £ n) by (15.41)(d). 

Apply (3.60) to obtain  (j £ i)Ù(i £ n) º (j £ i)Ù(i £ n)Ù(j £ n). 


ñ


 

(0 £ i) Ù(i £ n) Ù(0 £ j) Ù(j £ i)Ù(j £ n) 
 


á

 (0 £ j) Ù(j £ i) Þ (0 £ i) by (15.41)(d). 

Apply (3.60) to obtain  (0 £ i) Ù(0 £ j) Ù(j £ i) º (0 £ j) Ù(j £ i) . 


ñ


 

(i £ n) Ù(0 £ j) Ù(j £ i)Ù(j £ n) 
 

 

(0 £ j) Ù(j £ n) Ù(j £ i) Ù(i £ n) 
 

 

 

The proof uses (15.41)(d), the transitivity property for £ .
For the step which uses (8.21), choose k and l fresh
variables. Then apply (8.21) to rename the dummy i to k and
afterwards (8.21) to rename the dummy j to l. As there are no free
occurrences of i or j now ``reverse'' by renaming k to j and
then l to i. To formalize write down (8.21) in each case and apply
Transitivity three times.
We have already discussed (8.13) Axiom, Empty Range. For
(8.14) Axiom, Onepoint rule observe that there is a
restriction that there are no free occurrences of the object variable
x in the expression E. The following examples show what can happen if one ignores
this restriction:
Consider
(+x  x = x^{2}2x+2:x) = x^{2}2x +2
and
("x  x = x^{2}x +1: x = 1) º (x^{2}x+1 = 1)