Hola.
Tenés razón, yo me refería al lema L10_5 :)
Me alegro que te haya quedado entonces una prueba fácil de seguir. Aquí la clave es la eleccón del testigo del exists, ya que luego (como vos decís) se resuelve esencialmente con reemplazos de prodS, prod0 y sum0.
Saludos, Carlos