OneToOneFunction | *documentation* The Class of UnaryFunctions which are one to one. 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) | |

**has axiom** (*<=>* (*instance* ?FUN OneToOneFunction) (forall (?ARG1 ?ARG2) (=> (*and* (*instance* ?ARG1 (*DomainFn* ?FUN)) (*instance* ?ARG2 (*DomainFn* ?FUN)) (*not* (*equal* ?ARG1 ?ARG2))) (*not* (*equal* (*AssignmentFn* ?FUN ?ARG1) (*AssignmentFn* ?FUN ?ARG2))))))
| |

**is a kind of** UnaryFunction | |

BinaryRelation | **is first ***domain* of *DomainFn* | |

**is first ***domain* of *equivalenceRelationOn* | |

**is first ***domain* of *inverse* | |

**is first ***domain* of *irreflexiveOn* | |

**is first ***domain* of *partialOrderingOn* | |

**is first ***domain* of *RangeFn* | |

**is first ***domain* of *reflexiveOn* | |

**is first ***domain* of *totalOrderingOn* | |

**is first ***domain* of *trichotomizingOn* | |

**is second ***domain* of *inverse* | |

Function | **is first ***domain* of *AssignmentFn* | |

**is first ***domain* of *closedOn* | |

**is first ***domain* of *range* | |

**is first ***domain* of *rangeSubclass* | |

Class | **is third ***domain* of *domain* | |

**is third ***domain* of *domainSubclass* | |

Abstract | **is ***disjoint* from Physical | |