*AdditionFn* | *documentation* If ?NUMBER1 *and* ?NUMBER2 are Numbers, then (*AdditionFn* ?NUMBER1 ?NUMBER2) is the arithmetical sum of these numbers | |

**has axiom** (*<=>* (*equal* (*RemainderFn* ?NUMBER1 ?NUMBER2) ?NUMBER) (*equal* (*AdditionFn* (*MultiplicationFn* (*FloorFn* (*DivisionFn* ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
| |

**has domain1** Quantity | |

**has domain2** Quantity | |

**has ***identityElement* 0 | |

**has ***range* Quantity | |

**is an ***instance* of AssociativeFunction | |

**is an ***instance* of CommutativeFunction | |

**is an ***instance* of RelationExtendedToQuantities | |

BinaryFunction | **is first ***domain* of *distributes* | |

**is first ***domain* of *identityElement* | |

**is second ***domain* of *distributes* | |

Relation | **is first ***domain* of *domain* | |

**is first ***domain* of *domainSubclass* | |

**is first ***domain* of *holds* | |

**is first ***domain* of *subrelation* | |

**is first ***domain* of *valence* | |

**is second ***domain* of *subrelation* | |

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

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

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