2. e : B
B
3. IsEqFun(B;e)
4. a :
5. f :
aB
6. Surj(
a; B; f)
7. y : B
8. (
x.(f(x)) e y) 
{p:(a)| 
i:a. p(i) }
9. (f(least i:
. (f(i)) e y)) e y
f(least x:. (f(x)) e y) = yB
aB
a; B; f)
x.(f(x)) e y) {p:(a)| i:a. p(i) }
. (f(i)) e y)) e y
f(least x:. (f(x)) e y) = y| By: |
|
| 1 |
f(least i:. (f(i)) e y) B | 3 steps |
| 2 |
y B | Auto |
| 3 |
. (f(i)) e y) = y
f(least x:. (f(x)) e y) = y | Auto |
About:
 |  |  |  |  |  |
 |  |  |  |  |