proposition: Lemma fimfunE T (R : ringType) (f : {fimfun T >-> R}) x : f x = \sum_(y \in range f) (y * \1_(f @^-1` [set y]) x).
proof: Proof. rewrite (fsbigD1 (f x))// /= indicE mem_set// mulr1 fsbig1 ?addr0//. by move=> y [fy /= /nesym yfx]; rewrite indicE memNset ?mulr0. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure numfun