PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
one
one
preser
fin
1
1
1
1
1
1
1.
T:
Type
2.
S:
Type
3.
n:
4.
f:
n
T
5.
Bij(
n; T; f)
6.
f1:
T
S
7.
g:
S
T
8.
g o f1 = Id
9.
f1 o g = Id
Bij(
n; S; f1 o f)
By:
Analyze 0
THEN
Analyze 0
Generated subgoals:
1
10.
a1:
n
a2:
n. (f1 o f)(a1) = (f1 o f)(a2)
a1 = a2
2
10.
b:
S
a:
n. (f1 o f)(a) = b
About:
n
a2:n. (f1 o f)(a1) = (f1 o f)(a2) 
a1 = a2 
a:n. (f1 o f)(a) = bn
Tn; T; f)ST Bij(n; S; f1 o f)n a2:n. (f1 o f)(a1) = (f1 o f)(a2) a1 = a2 a:n. (f1 o f)(a) = b
