for n, k being Nat holds { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } is finite