行列の積は定義ですよね。横と縦を掛けて足すやつ。
あれを定理だという人はいないだろう。
「行列という概念を導入した段階」では「行列の積」というものは「存在しない」。
行列の積を「定義」して初めてそういうものが存在し得るというわけだ。
では実数においていくつかの公理（分配法則など）を設定した段階で、
「数のマイナス×マイナスという概念」は「存在」しているのだろうか？
存在していないのであれば「定義」するしかないのではないだろうか？