f:(A onto
B), a:
. a onto A 
(B Discrete) Surj(A; B; f)
(
e:(A
A
). x,y:A. (x e y) x = y)f:(B onto C), g:(A onto B). f o g 
A onto Ck:, p:{p:(k)| i:k. p(i) }. (least i:. p(i)) kk:, p:{p:(k)| i:k. p(i) }. p(least i:. p(i))