exponent
Sections
AutomataTheory
Doc
Def
Bij(A; B; f) == Inj(A; B; f) & Surj(A; B; f)
Thm*
n,m:
.
f:((
m
n)
(n
m)). Bij(
m
n;
(n
m); f) fun_enumer
In prior sections:
fun
1
finite
sets
n,m:
. 
f:((m
n)(n
m)). Bij(mn; (nm); f) fun_enumer
n,m:. f:((mn)(nm)). Bij(mn; (nm); f) fun_enumer