/* * Between finite sets of the same size, total surjections are bijections. */ MACHINE SurjBij INCLUDES ParFun, DomRan ASSERTIONS !(ss, tt) . (ss : FIN(INTEGER) & tt : FIN(INTEGER) & card(ss) = card(tt) => (ss -->> tt) <: (ss >->> tt)) END