How multiplication is defined in Peano arithmetic