Nuprl - Pf prod_fin_is_fin 1 2 6 2 1 1 1 3 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

f((an+a1) n) = b1

By: Assert (a = ((an+a1) n))

Generated subgoals:

1 a = ((an+a1) n) n

2 14. a = ((an+a1) n) n
f((an+a1) n) = b1

About:

1	`a = ((an+a1) n) n`
2	14. `a = ((an+a1) n) n` `f((an+a1) n) = b1`