g:(A'
A). Bij(A'; A; g) 
(x:A. B(x)) ~ (x':A'. B(g(x')))f:(AB). Bij(A; B; f) (
g:(BA). InvFuns(A;B;f;g)) InvFuns(B;A;g;f)| Theorem | Name |
| g:(A'A). Bij(A'; A; g) (x:A. B(x)) ~ (x':A'. B(g(x'))) | [one_one_corr_fams_if_bij_A] |
| cites the following: | |
| f:(AB). Bij(A; B; f) (g:(BA). InvFuns(A;B;f;g)) | [bij_imp_exists_inv2] |
| InvFuns(B;A;g;f) | [inv_funs_2_sym] |
| [inv_funs_2_identity] |