'a,'b:S.
  all(f:'a  'b. equal(onto(f),all(y:'b. exists(x:'a. equal(y,f(x))))))

1

1. 'a : S 2. 'b : S 3. f : 'a'b   (onto('a;'b;f)) = (y:'b. (x:'a. (y = (f(x)))))

3 steps

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