In Tao's analysis volume 1, I am introduced to this thing called the axiom of substitution. While constructing real numbers from rationals, he defined reals to be formal limits of Cauchy sequences of rationals. He said $\lim a_n=\lim b_n$ iff $(a_n)$ and $(b_n)$ are equivalent sequences. Then he defines addition of reals as - $\lim a_n + \lim b_n=\lim(a_n+b_n)$. Then he verifies that the axiom of substitution is not violated i.e. if $x=x'$ then $x+y=x'+y$. (I like to state this as "addition is well-defined").
My question : It seems that the axiom of substitution is a rather fundamental one that one needs to verify whenever a binary operation (such as addition) is introduced. However, not once in our course on group theory did we verify this axiom when we defined a binary operation on a set (and tried to show it forms a group). Shouldn't it be the first step?