proposition: Lemma fimfunEord T (R : ringType) (f : {fimfun T >-> R}) (s := fset_set (f @` setT)) : forall x, f x = \sum_(i < #|`s|) (s`_i * \1_(f @^-1` [set s`_i]) x).
proof: Proof. move=> x; rewrite fimfunE fsbig_finite//= (big_nth 0)/= big_mkord. exact: eq_bigr. 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