2. f :
a bij
a
3. f
a onto a
4. f
a
a
5. Bij(
a; a; f)
6. (
y.least x:. f(x)=
y) aa
7. Inj(
a; a; y.least x:. f(x)=y)
8. x :
a
9. f(least x@0:
. f(x@0)=f(x)) = f(x)
(least x@0:. f(x@0)=f(x)) = x a
a bij a
a onto a
aa
a; a; f)
y.least x:. f(x)=y) aa
a; a; y.least x:. f(x)=y)
a
. f(x@0)=f(x)) = f(x)
(least x@0:. f(x@0)=f(x)) = x a| By: |
. <bool>) BackThru: Inj(a; a; f) |
| 1 |
Inj(a; a; f) | 1 step |
| 2 |
(least x@0:. f(x@0)=f(x)) a | 1 step |
About:
 |  |  |  |  |  |