In the paper a characterization of Moufang loops by right division is investigated. If \((M,\cdot)\) is a Moufang loop (i.e., a loop satisfying the identity \(x\cdot(y\cdot(x\cdot z))=((x\cdot y)\cdot x)\cdot z\)) and we put \(x*y=x\cdot y^{-1}\) for all \(x,y\in M\) then \((M,*)\) is a quasigroup satisfying the identity \(x*[(z*x)*y]=[x*(((x*x)*x)*y)]*z\) (Lemma 1). Conversely, if a quasigroup \((Q,*)\) satisfies this identity and we put \(x\cdot y=x*((y*y)*y)\) for all \(x,y\in Q\) then \((Q,\cdot)\) is a Moufang loop (Theorem 1). The construction was first carried out using the software Prover9 and then an algebraic proof was obtained.