One author calls this a consequence of the field axioms. If this is true, then we wouldn’t want to call it an axiom since it has been proven.
The idea extends to functions:
- a+c=b+c, a=b
- f(x)+c=g(x)+c, f(x)=g(x)
We found it expressed differently, and believe this form is harder to “see”:
a=b, c=d, a+c=b+d