This is a continuation of my previous question A unitarity axiom in the vector space axioms concerning the unitarity law $1\cdot\boldsymbol x =\boldsymbol x$ in the set of axioms defining the vector space $V$ over a field $F$: \begin{align} \alpha\cdot(\beta\cdot\boldsymbol x)&=(\alpha\,\beta)\cdot\boldsymbol x,\tag1\\ (\alpha+\beta)\cdot\boldsymbol x&=\alpha\cdot\boldsymbol x+\beta\cdot\boldsymbol x,\tag2\\ \alpha\cdot(\boldsymbol x +\boldsymbol y)&=\alpha\cdot\boldsymbol x+\alpha\cdot\boldsymbol y,\tag3\\ 1\cdot\boldsymbol x &=\boldsymbol x\,.\tag4 \end{align} I do not display here the remaining axioms of a commutative group $G=\{+;\boldsymbol x,\boldsymbol y,\ldots\}$ and of the field $F$ above.
We thus have defined set of objects $\boldsymbol x,\boldsymbol
y,\ldots\in V$ supplemented with an external object set
$\alpha,\beta,\ldots\in F$ and interbred them by $(1){-}(4)$. The axiom
$(4)$ is needed to identify the formally independent elements
$\boldsymbol x$ and $1\cdot\boldsymbol x$. This was nicely
elucidated to me by user lhf in the post mentioned above.
Well, let us redefine the $V\to \tilde V$ to be a set of the ordered pairs $(\alpha,\boldsymbol x)\ni\tilde V$ being equivalent to the objects $\alpha\cdot\boldsymbol x\ni V$, and their formal (group) sums $(\alpha,\boldsymbol x)+(\beta,\boldsymbol y)+\cdots\equiv (\gamma,\boldsymbol z)$. It is also assumed that symbols $\boldsymbol x,\boldsymbol y,\boldsymbol z,\ldots$ belong to some infinite set $S$. It follows that we may rewrite the rules $(1){-}(4)$ in the form \begin{align*} (\alpha,(\beta,\boldsymbol x))&=(\alpha\,\beta,\boldsymbol x),\\ (\alpha+\beta,\boldsymbol x)&=(\alpha,\boldsymbol x)+(\beta,\boldsymbol x),\\ (\gamma,(\alpha,\boldsymbol x) +(\beta,\boldsymbol y))&=(\gamma\,\alpha,\boldsymbol x)+(\gamma\,\beta,\boldsymbol y),\tag5 \end{align*} which counts one fewer axiom than $(1){-}(4)$.
Hereof I conclude that axiom $(4)$ carries just a $\textit{nomenclature}$ meaning and does not touch the algebraic mathematics $(1){-}(3)$ itself. That is notation change $\alpha\cdot\boldsymbol x\rightleftarrows(\alpha,\boldsymbol x)$, $\boldsymbol x\rightleftarrows (1,\boldsymbol x)$; not more. In contrast to this, I $\textit{cannot get rid of}$ $(1){-}(3)$ by any change of notation.
It seems that I can thus formally use this version of the vector space algebra without loss of further generality. May I spare $(4)$ by that or any other way?
PS. Perhaps undefined working rules with (vague) objects/sums like \begin{equation*} (\alpha,\boldsymbol x)+(\beta,\boldsymbol y)+\cdots \end{equation*} miss here. Well, what about \begin{equation*} (\gamma,(\alpha,\boldsymbol x) +(\beta,\boldsymbol y)+\cdots)=(\gamma\,\alpha,\boldsymbol x)+(\gamma\,\beta,\boldsymbol y)+\cdots\,\quad? \end{equation*} which follows from recursive associativity wrt group action $+$: \begin{equation*} A+B+\cdots=A+(B+\cdots). \end{equation*} This is exactly sum of two elements as $(5)$ requires. To put it differently, if the rule $(4)$ can be actually hidden by certain renotation then this axiom is really fictituous and may be discarded in a way.