pm#one_to_one_function_type  a function F is one to one just in case for all X, Y in the domain of F, if X is not identical to Y, then F(X) is not identical to F(Y)
  supertype:  pm#unary_function_type  class of functions requiring a single argument; if R is functional, then if R(x -> y) and P(x -> z) then y=z
  equal:  sumo#one_to_one_function (pm)
  subtype:  pm#sequence_function_type  class of one_to_one_functions whose range is a subclass of the positive_integers

No statement uses or specializes pm#one_to_one_function_type; click here to add one.