e:(B
B
).
Thm* IsEqFun(B;e)
(a:
, f:(a onto
B), y:B. (least x:. (f(x)) e y) 
a)k:, p:{p:(k)| 
i:k. p(i) }. (least i:. p(i)) k| Rank | Theorem | Name |
| 2 | e:(BB).
Thm* IsEqFun(B;e) (a:, f:(a onto B), y:B. (least x:. (f(x)) e y) a) | [nsub_surj_least_preimage_total_gen] |
| cites the following: | ||
| 1 | k:, p:{p:(k)| i:k. p(i) }. (least i:. p(i)) k | [least_wf] |