proposition: Lemma esum_image (R : realType) (T T' : choiceType) (P : set T) (e : T -> T') (a : T' -> \bar R) : set_inj P e -> \esum_(j in e @` P) a j = \esum_(i in P) a (e i).
proof: Proof. by move=> /inj_bij; apply: reindex_esum. 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