$\newcommand{\Z}{\mathbb{Z}}
\newcommand{\Q}{\mathbb{Q}}$

I think the notion of "well-defined" may not always be well defined and should perhaps be avoided. In your example, it may be unclear what exactly is being proved. 

I also think it is all right to introduce notions within a statement; this can be done without ambiguity by using terms such as "define" and "introduce" and/or the symbol "$:=$" meaning "[is] defined as". I have done it many times in my papers and never had a reviewer complain about that. In particular, your example could be rewritten as follows. 

>**Proposition** 

>(I) The binary relation $\sim$ on $P:=\Z\times\Z^*$ defined by the condition 
\begin{equation}
(p_1,q_1)\sim(p_2,q_2)\iff p_1q_2=p_2q_1	
\end{equation}
for $(p_1,q_1)$ and $(p_2,q_2)$ in $P$ is an equivalence. Let then 
\begin{equation}
	\Q:=P/\sim. 
\end{equation}

>(II) Consider the binary operations $\oplus$ and $\odot$ on $P$ defined by the formulas 
\begin{align}
	(p_1,q_1)\oplus(p_2,q_2)&:=(p_1q_2+p_2q_1,q_1q_2), \\ 
	(p_1,q_1)\odot(p_2,q_2)&:=(p_1p_2,q_1q_2) 
\end{align}
for $(p_1,q_1)$ and $(p_2,q_2)$ in $P$. Then for any $r_1,\tilde r_1,r_2,\tilde r_2$ in $P$ such that $r_1\sim\tilde r_1$ and $r_2\sim\tilde r_2$ we have 
\begin{equation}
	r_1\oplus r_2\sim\tilde r_1\oplus\tilde r_2\quad\text{and}\quad r_1\odot r_2\sim\tilde r_1\odot\tilde r_2. 
\end{equation}
Define now the binary operations $+$ and $\cdot$ on $\Q$ by the formulas  
\begin{equation}
	[r_1]+[r_2]:=[r_1\oplus r_2]\quad\text{and}\quad [r_1]\cdot[r_2]:=[r_1\odot r_2] 
\end{equation}
for all $r_1,r_2$ in $P$. 
Let also $0_\Q:=[(0,1)]$, and $1_\Q:=[(1,1)]$. Then $(\Q,+,\cdot,0_\Q,1_\Q)$ is a field. 

*Proof.* $\ldots$