f:(
a onto
b), y:b. (least x:. f(x)=
y) 
ab;
i,j. i=j)e:(B
B
).
Thm* IsEqFun(B;e)
(a:, f:(a onto B), y:B. (least x:. (f(x)) e y) a)| Rank | Theorem | Name |
| 3 | f:(a onto b), y:b. (least x:. f(x)=y) a | [nsub_surj_least_preimage_total] |
| cites the following: | ||
| 1 | b;i,j. i=j) | [eq_int_is_eq_nsub] |
| 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] |