Nuprl - Pf prod_fin_is_fin 1 2 6 2 1 1 1

PrintForm Definitions finite sets Sections AutomataTheory Doc

1. T: Type
2. t: T
3. n:
4. f: nT
5. Inj(n; T; f)
6. b:T. a:n. f(a) = b
7. n > 0
8. b1: T
9. b2: T
10. a: n
11. f(a) = b1
12. a1: n
13. f(a1) = b2

a:(nn). (x. < f(x n),f(x rem n) > )(a) = < b1,b2 >

By: InstConcl [an+a1]

Generated subgoals:

1 0an+a1

2 an+a1 < nn

3 (x. < f(x n),f(x rem n) > )(an+a1) = < b1,b2 >

4 14. a2: (nn)
(x. < f(x n),f(x rem n) > )(a2) TT

About:

1	`0an+a1`
2	`an+a1 < nn`
3	`(x. < f(x n),f(x rem n) > )(an+a1) = < b1,b2 >`
4	14. `a2:` `(nn)` `(x. < f(x n),f(x rem n) > )(a2) TT`