proposition: Lemma fset_set_comp (T1 : Type) (T2 T3 : choiceType) (D : set T1) (f : {fimfun T1 >-> T2}) (g : T2 -> T3) : fset_set [set (g \o f) x | x in D] = [fset g x | x in fset_set [set f x | x in D]]%fset.
proof: Proof. by rewrite -(image_comp f g) fset_set_image. 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