proposition: Lemma SubsetUnionRightIntegrable : forall {I J : IntegrationSpace} (hn : list (@ProdIntegrable I J)), IntegrableSet (SubsetUnion (map prodint_g hn)).
proof: Proof. induction hn. - apply (IntegrableFunctionExtensional (Xconst (X (ElemFunc J)) 0)). split. + intros x _. right. intro abs. contradiction. + intros. simpl. destruct xG. contradiction. reflexivity. + apply IntegrableZero. - apply IntegrableSetUnion. apply a. apply IHhn. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile