
 S
S s:S. Dec(
s:S. Dec( t:T. f(t) = s)
t:T. f(t) = s) t:T. f(t) = s }
t:T. f(t) = s }
 T
T s:{s:S|
s:{s:S|  t:T. f(t) = s }. f(f@0(s)) = s
t:T. f(t) = s }. f(f@0(s)) = s Bij({s:S|
 Bij({s:S|  t:T. f(t) = s }; x,y:T//(f(x) = f(y)); f@0)
t:T. f(t) = s }; x,y:T//(f(x) = f(y)); f@0)| 1 | 9. a1: {s:S|  t:T. f(t) = s }    a2:{s:S|  t:T. f(t) = s }. f@0(a1) = f@0(a2)  x,y:T//(f(x) = f(y))   a1 = a2 | 
| 2 | 9. b: x,y:T//(f(x) = f(y))    a:{s:S|  t:T. f(t) = s }. f@0(a) = b  x,y:T//(f(x) = f(y)) | 
About:
|  |  |  |  |  | 
|  |  |  |  |