n ~ Alph5. EquivRel x,y:Alph*. x E y
6.
x,y:Alph*. Dec(x E y)
h:(Alph*
Alph*). (x,y:Alph*. (x E y) 
h(x) = h(y)) & (x:Alph*. x E (h(x)))Alph*Propf:(nAlph). Bij(n; Alph; f)x,y:Alph*. Dec(x E y) h:(Alph*Alph*). (x,y:Alph*. (x E y) h(x) = h(y)) & (x:Alph*. x E (h(x)))f:(AB). Bij(A; B; f)) (A ~ B))
4| 1 | 4. n ~ Alph 5. EquivRel x,y:Alph*. x E y 6. x,y:Alph*. Dec(x E y) h:(Alph*Alph*). (x,y:Alph*. (x E y) h(x) = h(y)) & (x:Alph*. x E (h(x))) |
About:
 |  |  |  |  |
 |  |  |  |  |