PrintForm
Definitions
automata
5
Sections
AutomataTheory
Doc
At:
surj
is
inj
gen
1
1
1
1
2
1
1
1
1
2
1
1
1
1.
A:
Type
2.
B:
Type
3.
f:
A
B
4.
f1:
A
B
5.
g:
B
A
6.
InvFuns(A; B; f1; g)
7.
n:
8.
f2:
n
B
9.
g1:
B
n
10.
g1 o f2 = Id
11.
f2 o g1 = Id
12.
Surj(A; B; f)
13.
a1:
A
14.
a2:
A
15.
f(a1) = f(a2)
16.
g1(f1(a1)) = g1(f1(a2))
17.
f1(a1) = f1(a2)
a1 = a2
By:
ApFunToHypEquands `z' (g(z)) A 17
Generated subgoal:
1
18.
g(f1(a1)) = g(f1(a2))
a1 = a2
About:
a1 = a2
BBA
nBn a1 = a2 a1 = a2
