PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
prod
fin
is
fin
1
2
6
1
1
2
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:
(n
n)
0
(a1
n)
By:
BackThru
Thm*
a:
, n:
. 0
(a
n)
Generated subgoals:
None
About:
n
T
a1,a2:n. f(a1) = f(a2) 
a1 = a2n; T; f)(n
n)(nn)
0
(a1 
n)a:, n:
. 0(a n)
