IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
finite-partition21211 1. n : 2. 0<n 3. k : 4. c : nk 5. p : k( List)
6. sum(||p(j)|| | j < k) = n-1
7. j:k, x,y:||p(j)||. x<y (p(j))[x]>(p(j))[y]
8. j:k, x:||p(j)||. (p(j))[x]<n-1 & c((p(j))[x]) = j sum(if c(n-1)=j 1 else 0 fi | j < k) = 1
By:
Inst
Thm*n:, f:(n), m:n.
Thm* (x:n. x = mf(x) = 0) sum(f(x) | x < n) = f(m)
[k;j. if c(n-1)=j 1 else 0 fi;c(n-1)]