(
k:
, f:(k
A). f 
k onto
{a:A| 
i:k. a = f(i) })Thm*
Thm* (
k:, f:(kA).
Thm* ({a:A|
i:k. a = f(i) } Type
Thm* (& f
k{a:A| i:k. a = f(i) }
Thm* (& Surj(
k; {a:A| i:k. a = f(i) }; f))| Rank | Theorem | Name |
| 3 | (k:, f:(kA). f k onto {a:A| i:k. a = f(i) }) | [nsub_discr_range_surjtype] |
| cites the following: | ||
| 2 | Thm*
Thm* ( k:, f:(kA).
Thm* ({a:A| i:k. a = f(i) } Type
Thm* (& f k{a:A| i:k. a = f(i) }
Thm* (& Surj( k; {a:A| i:k. a = f(i) }; f)) | [nsub_discr_range_surj] |