n; T; f)7. Surj(
n; T; f)8.
t:T. Dec(R(t))9. b: T
10.
b = f(n-1)
a:(n-1). f(a) = b 
{t:T| t = f(n-1) }
PropnTn; T; f)t:T. Dec(R(t))b = f(n-1) a:(n-1). f(a) = b {t:T| t = f(n-1) }| 1 | 6. Inj(n; T; f) 7. Surj( n; T; f)8. t:T. Dec(R(t))9. b: T 10. b = f(n-1) a:(n-1). f(a) = b {t:T| t = f(n-1) } |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |