At: prod fin is fin 1 2 6 1 1 1 1 1
1. T: Type
2. t: T
3. n: 
4. f: n
T
5. 
a1,a2:n. f(a1) = f(a2) 
a1 = a2
6. Surj(n; T; f)
7. n > 0
8. a1: (n
n)
9. a2: (nn)
10. f(a1 
n) = f(a2 n)
11. f(a1 rem n) = f(a2 rem n)
0
(a1 n)
By: BackThru
Thm* a:, n:
. 0(a n)
Generated subgoals:None
About:
