[isabelle] Decomposing an Infinite Sum

Dear Isabelle/HOL experts and users,
  I am trying to prove a lemma about an infinite sum of zeros, but I can
only prove it assuming that some set is finite. Is there a way to prove it
without this restriction?


I proved lemma qValSumAunrestricted,
but I want to prove lemma qValSumAunrestrictedGeneral
in the following file:

Kind Regards,
José Manuel Rodriguez Caballero

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.