Nuprl - Pf fun_enumer 1 2 1 2 2 1

PrintForm Definitions exponent Sections AutomataTheory Doc

1. n:
2. m:
3. 0 < m
4. f: ((m-1)n)(nm-1)
5. Bij((m-1)n; (nm-1); f)
6. n = 0
7. f1: n(nm-1)(n(nm-1))
8. Bij(n(nm-1); (n(nm-1)); f1)

f:((mn)(nm)). Bij(mn; (nm); f)

By: Assert (n(nm-1) = (nm))

Generated subgoals:

1 n(nm-1) = (nm)

2 9. n(nm-1) = (nm)
f:((mn)(nm)). Bij(mn; (nm); f)

About:

1	`n(nm-1) = (nm)`
2	9. `n(nm-1) = (nm)` `f:((mn)(nm)). Bij(mn; (nm); f)`