k inj
k) =ext (k bij k)k inj k) =ext (k onto k) B) 
(A inj B)| Rank | Theorem | Name |
| 8 | k inj k) =ext (k bij k) | [nsub_inj_exteq_nsub_bij] |
| cites the following: | ||
| 7 | k inj k) =ext (k onto k) | [nsub_inj_exteq_nsub_surj] |
| 0 | B) (A inj B) | [bijtype_sub_injtype] |