Suppose that $X$ and $Y$ are sets and that $\sim$ is an equivalence relation on $X$. Further assume that one wants to define a function $f:X/\sim \to Y$. In order for $f$ to be a function, the usual difficulty is to show that it is well defined. This means that for any $(x,y), (x,z) \in f$ we need to have $y=z$. My question is, is it allowed to use the notation $f(x)$ prior to showing this?
More precisely, when trying to prove that $f$ is well defined, we might say let $x=[a]$ and $x=[b]$ be two representations with $a,b \in X$. Then we need to show that $f([a])=f([b])$. Here we are using the functional notation before knowing that it actually is a function. I am not sure if this is "usual" or even done at all, since usually functional notation is only used when the defined object is unique. However, since the linked article is concerned with formal logic and not "everyday mathematics" im not sure if its still fine to use it prior to actually showing well definedness.
In this question the agreed upon opinion seems to be that it is not allowed to do that. However, I think this is done in an analogous way when talking about essentially unique objects anyways. So for example, when defining the tensor product $A \otimes B$ we only get that this is essentially unique but still use a functional symbol to denote this. Another example can be found in $\epsilon-\delta$ proofs, where one often writes $\forall \epsilon >0 \exists \delta_{\epsilon} (...)$. Strictly speaking, $\delta_{\epsilon}$ is also a function symbol but obviously the existence of it is not unique, so when using this notation, we dont infer $\delta_{\epsilon}=\delta_{\epsilon'}$ when $\epsilon=\epsilon'$. So as far as I can tell, one usually doesn't care too much about notation here, as long as one is sufficiently careful with the inferences. Thus, as long as I don't infer that $f(a)=f(b)$ whenever $a=b$, using the notation prior to proving $f$ is well defined should do no harm, should it?