Nuprl - Pf prod_fin_is_fin 1 2 6 2 1 1

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

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

By: InstHyp [b1] 6 THEN Analyze -1 THEN InstHyp [b2] 6 THEN Analyze -1

Generated subgoal:

1 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 >

About: