proposition: Lemma esum1 [R : realFieldType] [I : choiceType] (D : set I) (a : I -> \bar R) : (forall i, D i -> a i = 0) -> \esum_(i in D) a i = 0.
proof: Proof. move=> a0; rewrite /esum (_ : [set _ | _ in _] = [set 0]) ?ereal_sup1//. apply/seteqP; split=> x //= => [[X [finX XI]] <-|->]. by rewrite fsbig1// => i /XI/a0. by exists set0; rewrite ?fsbig_set0//; exact: fsets_set0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology sequences normedtype numfun