PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
prod
fin
is
fin
1
2
6
2
1
1
1
1
1.
T:
Type
2.
t:
T
3.
n:
4.
f:
n
T
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
0
a
n+a1
By:
Inst
Thm*
a,b:
. 0
a
b [a;n]
Generated subgoals:
None
About:
T
b:T. 
a:
0
a
n+a1
