proposition: Lemma applyIntegralFst : forall { I J : IntegrationSpace } (l : list (@ProdIntegrable I J)) (x : X (ElemFunc I)) (lint : @IntegrableFunction (IntegrationSpaceCast J) (Xproj1 (ProdLFunc l) x)) (xD : Domain (IntegralFst (ProdLFunc l) (LElemProductIntegrableAE l)) x), partialApply _ x xD == Integral lint.
proof: Proof. intros. apply (@IntegralExtensional (IntegrationSpaceCast J)). intros. apply DomainProp. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile