proposition: Lemma fimfunE (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 fsbigop) mathcomp(functions cardinality set_interval) signed reals ereal topology normedtype sequences