2. k :
3. f :
(m+1)
(k+1)
4. Inj(
(m+1); (k+1); f)
5. a1 :
m
6. a2 :
m
7. (Replace value k by f(m) in f)(a1) = (Replace value k by f(m) in f)(a2)
8.
f(a1) = k
9. f(a2) = k
a1 = a2
(m+1)(k+1)
(m+1); (k+1); f)
m
m
f(a1) = k
a1 = a2| By: |
THEN Rewrite'7 by Thm: delete fenum value comp1 Using:[i:= a2] THEN Rewrite'7 by Thm: delete fenum value comp2 |
| 1 |
 k
8. f(a1) = k
9. f(a2) = k False | 1 step |
About:
 |  |  |  |  |  |  |  |  |