A confirmation by hand calculation that the Möbius ball is a gyrovector space (Q1685895)

\textit{A. A. Ungar} [Analytic hyperbolic geometry and Albert Einstein's special theory of relativity. Hackensack, NJ: World Scientific (2008; Zbl 1147.83004)] states on page 79 that the Möbius ball of any real inner product is a gyrocommutative gyrogroup, ``as one can readily check by computer algebra.'' The aim of this paper is to do the checking by hand, checking the axioms for gyrocommutative gyrogroups in an elementary manner. One can then show, as done by Ungar [loc. cit.], that the Möbius ball is a gyrovector space with a certain scalar multiplication called the Möbius scalar multiplication.