Def Surj(A;B;f) == b:B. a:A. f(a) = b

Thm* f:(AB). Surj(A;B;f) Prop