n,m:, f:(nm), p:(nn), q:(mm).
  Bij(n; n; p)
  
  Bij(m; m; q)
  
  sum(f(p(x),q(y)) | x < n; y < m) = sum(f(x,y) | x < n; y < m)

1

1. n :  2. m :  3. f : nm 4. p : nn 5. q : mm 6. Bij(n; n; p) 7. Bij(m; m; q)   sum(sum(f(p(x),q(y)) | y < m) | x < n) = sum(sum(f(x,y) | y < m) | x < n)

4 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html