Nuprl - Pf fun_enumer 1 2 1

1. n:
2. m:
3. 0 < m
4. f: ((m-1)n)(nm-1)
5. Bij((m-1)n; (nm-1); f)

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

By: Decide (n = 0)

Generated subgoals:

1 6. n = 0
f:((mn)(nm)). Bij(mn; (nm); f)

2 6. n = 0
f:((mn)(nm)). Bij(mn; (nm); f)

About:

1	6. `n = 0` `f:((mn)(nm)). Bij(mn; (nm); f)`
2	6. `n = 0` `f:((mn)(nm)). Bij(mn; (nm); f)`