Nuprl - Pf prod_fin_is_fin 1 2 6 1 1 1 1

PrintForm Definitions finite sets Sections AutomataTheory Doc

1. T: Type
2. t: T
3. n:
4. f: nT
5. a1,a2:n. f(a1) = f(a2) a1 = a2
6. Surj(n; T; f)
7. n > 0
8. a1: (nn)
9. a2: (nn)
10. f(a1 n) = f(a2 n)
11. f(a1 rem n) = f(a2 rem n)

a1 = a2

By: InstHyp [a1 n;a2 n] 5 THEN InstHyp [a1 rem n;a2 rem n] 5

Generated subgoals:

1 0(a1 n)

2 (a1 n) < n

3 0(a2 n)

4 (a2 n) < n

5 12. (a1 n) = (a2 n) n
0(a1 rem n)

6 12. (a1 n) = (a2 n) n
(a1 rem n) < n

7 12. (a1 n) = (a2 n) n
0(a2 rem n)

8 12. (a1 n) = (a2 n) n
(a2 rem n) < n

9 12. (a1 n) = (a2 n) n
13. (a1 rem n) = (a2 rem n) n
a1 = a2

About:

1	`0(a1 n)`
2	`(a1 n) < n`
3	`0(a2 n)`
4	`(a2 n) < n`
5	12. `(a1 n) = (a2 n) n` `0(a1 rem n)`
6	12. `(a1 n) = (a2 n) n` `(a1 rem n) < n`
7	12. `(a1 n) = (a2 n) n` `0(a2 rem n)`
8	12. `(a1 n) = (a2 n) n` `(a2 rem n) < n`
9	12. `(a1 n) = (a2 n) n` 13. `(a1 rem n) = (a2 rem n) n` `a1 = a2`